Theorem con3bi ≪ | index | src | ≫

theorem con3bi (a b: wff): $ a -> b <-> ~b -> ~a $;

Step	Hyp	Ref	Expression
1		con3	(a -> b) -> ~b -> ~a
2		ax_3	(~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)