Theorem con1bi ≪ | index | src | ≫ 

theorem con1bi (a b: wff): $ ~a -> b <-> ~b -> a $;
StepHypRefExpression
1 con1 
(~a -> b) -> ~b -> a
2 con1 
(~b -> a) -> ~a -> b
3 1, 2 ibii 
~a -> b <-> ~b -> a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)