Theorem aleq ≪ | index | src | ≫ 

theorem aleq {x: nat} (a b: wff x): $ A. x (a <-> b) -> (A. x a <-> A. x b) $;
StepHypRefExpression
1 ax_4 
A. x (a -> b) -> A. x a -> A. x b
2 bi1 
(a <-> b) -> a -> b
3 2 alimi 
A. x (a <-> b) -> A. x (a -> b)
4 1, 3 syl 
A. x (a <-> b) -> A. x a -> A. x b
5 ax_4 
A. x (b -> a) -> A. x b -> A. x a
6 bi2 
(a <-> b) -> b -> a
7 6 alimi 
A. x (a <-> b) -> A. x (b -> a)
8 5, 7 syl 
A. x (a <-> b) -> A. x b -> A. x a
9 4, 8 ibid 
A. x (a <-> b) -> (A. x a <-> A. x b)

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp), axs_pred_calc (ax_gen, ax_4)