Theorem anrass | index | src |

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

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)