Theorem con1 ≪ | index | src | ≫

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

Step	Hyp	Ref	Expression
1		notnot1	b -> ~~b
2	1	imim2i	(~a -> b) -> ~a -> ~~b
3	2	a3d	(~a -> b) -> ~b -> a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)