Theorem an4 ≪ | index | src | ≫ 

theorem an4 (a b c d: wff): $ a /\ b /\ (c /\ d) <-> a /\ c /\ (b /\ d) $;
StepHypRefExpression
1 bitr4 
(a /\ b /\ (c /\ d) <-> a /\ (b /\ (c /\ d))) -> (a /\ c /\ (b /\ d) <-> a /\ (b /\ (c /\ d))) -> (a /\ b /\ (c /\ d) <-> a /\ c /\ (b /\ d))
2 anass 
a /\ b /\ (c /\ d) <-> a /\ (b /\ (c /\ d))
3 1, 2 ax_mp 
(a /\ c /\ (b /\ d) <-> a /\ (b /\ (c /\ d))) -> (a /\ b /\ (c /\ d) <-> a /\ c /\ (b /\ d))
4 bitr4 
(a /\ c /\ (b /\ d) <-> a /\ (c /\ (b /\ d))) -> (a /\ (b /\ (c /\ d)) <-> a /\ (c /\ (b /\ d))) -> (a /\ c /\ (b /\ d) <-> a /\ (b /\ (c /\ d)))
5 anass 
a /\ c /\ (b /\ d) <-> a /\ (c /\ (b /\ d))
6 4, 5 ax_mp 
(a /\ (b /\ (c /\ d)) <-> a /\ (c /\ (b /\ d))) -> (a /\ c /\ (b /\ d) <-> a /\ (b /\ (c /\ d)))
7 anlass 
b /\ (c /\ d) <-> c /\ (b /\ d)
8 7 aneq2i 
a /\ (b /\ (c /\ d)) <-> a /\ (c /\ (b /\ d))
9 6, 8 ax_mp 
a /\ c /\ (b /\ d) <-> a /\ (b /\ (c /\ d))
10 3, 9 ax_mp 
a /\ b /\ (c /\ d) <-> a /\ c /\ (b /\ d)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)