Theorem anlass | index | src |

theorem anlass (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 anass
a /\ b /\ c <-> a /\ (b /\ c)
3 1, 2 ax_mp
(a /\ b /\ c <-> b /\ (a /\ c)) -> (a /\ (b /\ c) <-> b /\ (a /\ c))
4 bitr
(a /\ b /\ c <-> b /\ a /\ c) -> (b /\ a /\ c <-> b /\ (a /\ c)) -> (a /\ b /\ c <-> b /\ (a /\ c))
5 ancomb
a /\ b <-> b /\ a
6 5 aneq1i
a /\ b /\ c <-> b /\ a /\ c
7 4, 6 ax_mp
(b /\ a /\ c <-> b /\ (a /\ c)) -> (a /\ b /\ c <-> b /\ (a /\ c))
8 anass
b /\ a /\ c <-> b /\ (a /\ c)
9 7, 8 ax_mp
a /\ b /\ c <-> b /\ (a /\ c)
10 3, 9 ax_mp
a /\ (b /\ c) <-> b /\ (a /\ c)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)