Theorem ordir ≪ | index | src | ≫ 

theorem ordir (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 orcomb 
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 ordi 
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 aneq 
(c \/ a <-> a \/ c) -> (c \/ b <-> b \/ c) -> ((c \/ a) /\ (c \/ b) <-> (a \/ c) /\ (b \/ c))
8 orcomb 
c \/ a <-> a \/ c
9 7, 8 ax_mp 
(c \/ b <-> b \/ c) -> ((c \/ a) /\ (c \/ b) <-> (a \/ c) /\ (b \/ c))
10 orcomb 
c \/ b <-> b \/ c
11 9, 10 ax_mp 
(c \/ a) /\ (c \/ b) <-> (a \/ c) /\ (b \/ c)
12 6, 11 ax_mp 
c \/ a /\ b <-> (a \/ c) /\ (b \/ c)
13 3, 12 ax_mp 
a /\ b \/ c <-> (a \/ c) /\ (b \/ c)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)