Theorem or12 ≪ | index | src | ≫ 

theorem or12 (a b c: wff): $ a \/ (b \/ c) <-> b \/ (a \/ c) $;
StepHypRefExpression
1 bitr3 
(~a /\ ~b -> c <-> a \/ (b \/ c)) -> (~a /\ ~b -> c <-> b \/ (a \/ c)) -> (a \/ (b \/ c) <-> b \/ (a \/ c))
2 impexp 
~a /\ ~b -> c <-> ~a -> ~b -> c
3 2 conv or 
~a /\ ~b -> c <-> a \/ (b \/ c)
4 1, 3 ax_mp 
(~a /\ ~b -> c <-> b \/ (a \/ c)) -> (a \/ (b \/ c) <-> b \/ (a \/ c))
5 bitr 
(~a /\ ~b -> c <-> ~b /\ ~a -> c) -> (~b /\ ~a -> c <-> b \/ (a \/ c)) -> (~a /\ ~b -> c <-> b \/ (a \/ c))
6 ancomb 
~a /\ ~b <-> ~b /\ ~a
7 6 imeq1i 
~a /\ ~b -> c <-> ~b /\ ~a -> c
8 5, 7 ax_mp 
(~b /\ ~a -> c <-> b \/ (a \/ c)) -> (~a /\ ~b -> c <-> b \/ (a \/ c))
9 impexp 
~b /\ ~a -> c <-> ~b -> ~a -> c
10 9 conv or 
~b /\ ~a -> c <-> b \/ (a \/ c)
11 8, 10 ax_mp 
~a /\ ~b -> c <-> b \/ (a \/ c)
12 4, 11 ax_mp 
a \/ (b \/ c) <-> b \/ (a \/ c)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)