Theorem andir ≪ | index | src | ≫ 

theorem andir (a b c: wff): $ (a \/ b) /\ c <-> a /\ c \/ b /\ c $;
StepHypRefExpression
1 bitr 
((a \/ b) /\ c <-> c /\ (a \/ b)) -> (c /\ (a \/ b) <-> a /\ c \/ b /\ c) -> ((a \/ b) /\ c <-> a /\ c \/ b /\ c)
2 ancomb 
(a \/ b) /\ c <-> c /\ (a \/ b)
3 1, 2 ax_mp 
(c /\ (a \/ b) <-> a /\ c \/ b /\ c) -> ((a \/ b) /\ c <-> a /\ c \/ b /\ c)
4 bitr 
(c /\ (a \/ b) <-> c /\ a \/ c /\ b) -> (c /\ a \/ c /\ b <-> a /\ c \/ b /\ c) -> (c /\ (a \/ b) <-> a /\ c \/ b /\ c)
5 andi 
c /\ (a \/ b) <-> c /\ a \/ c /\ b
6 4, 5 ax_mp 
(c /\ a \/ c /\ b <-> a /\ c \/ b /\ c) -> (c /\ (a \/ b) <-> a /\ c \/ b /\ c)
7 ancomb 
c /\ a <-> a /\ c
8 ancomb 
c /\ b <-> b /\ c
9 7, 8 oreqi 
c /\ a \/ c /\ b <-> a /\ c \/ b /\ c
10 6, 9 ax_mp 
c /\ (a \/ b) <-> a /\ c \/ b /\ c
11 3, 10 ax_mp 
(a \/ b) /\ c <-> a /\ c \/ b /\ c

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)