Theorem con2 ≪ | index | src | ≫

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

Step	Hyp	Ref	Expression
1		dne	~~a -> a
2		id	(a -> ~b) -> a -> ~b
3	1, 2	syl5	(a -> ~b) -> ~~a -> ~b
4	3	a3d	(a -> ~b) -> b -> ~a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)