theorem anass (a b c: wff): $ a /\ b /\ c <-> a /\ (b /\ c) $;
Step | Hyp | Ref | Expression |
1 |
|
anll |
a /\ b /\ c -> a |
2 |
|
anim1 |
(a /\ b -> b) -> a /\ b /\ c -> b /\ c |
3 |
|
anr |
a /\ b -> b |
4 |
2, 3 |
ax_mp |
a /\ b /\ c -> b /\ c |
5 |
1, 4 |
iand |
a /\ b /\ c -> a /\ (b /\ c) |
6 |
|
anim2 |
(b /\ c -> b) -> a /\ (b /\ c) -> a /\ b |
7 |
|
anl |
b /\ c -> b |
8 |
6, 7 |
ax_mp |
a /\ (b /\ c) -> a /\ b |
9 |
|
anrr |
a /\ (b /\ c) -> c |
10 |
8, 9 |
iand |
a /\ (b /\ c) -> a /\ b /\ c |
11 |
5, 10 |
ibii |
a /\ b /\ c <-> a /\ (b /\ c) |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp)