Theorem ordi ≪ | index | src | ≫ 

theorem ordi (a b c: wff): $ a \/ b /\ c <-> (a \/ b) /\ (a \/ c) $;
StepHypRefExpression
1 orim2 
(b /\ c -> b) -> a \/ b /\ c -> a \/ b
2 anl 
b /\ c -> b
3 1, 2 ax_mp 
a \/ b /\ c -> a \/ b
4 orim2 
(b /\ c -> c) -> a \/ b /\ c -> a \/ c
5 anr 
b /\ c -> c
6 4, 5 ax_mp 
a \/ b /\ c -> a \/ c
7 3, 6 iand 
a \/ b /\ c -> (a \/ b) /\ (a \/ c)
8 mpcom 
~a -> (~a -> b) -> b
9 8 conv or 
~a -> a \/ b -> b
10 mpcom 
~a -> (~a -> c) -> c
11 10 conv or 
~a -> a \/ c -> c
12 9, 11 animd 
~a -> (a \/ b) /\ (a \/ c) -> b /\ c
13 12 com12 
(a \/ b) /\ (a \/ c) -> ~a -> b /\ c
14 13 conv or 
(a \/ b) /\ (a \/ c) -> a \/ b /\ c
15 7, 14 ibii 
a \/ b /\ c <-> (a \/ b) /\ (a \/ c)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)