theorem alcomb {x y: nat} (a: wff x y): $ A. x A. y a <-> A. y A. x a $;
Step | Hyp | Ref | Expression |
1 |
|
alcom |
A. x A. y a -> A. y A. x a |
2 |
|
alcom |
A. y A. x a -> A. x A. y a |
3 |
1, 2 |
ibii |
A. x A. y a <-> A. y A. x a |
Axiom use
axs_prop_calc
(ax_1,
ax_2,
ax_3,
ax_mp),
axs_pred_calc
(ax_11)