Theorem contra ≪ | index | src | ≫

theorem contra (a: wff): $ (~a -> a) -> a $;

Step	Hyp	Ref	Expression
1		imidm	((~a -> a) -> (~a -> a) -> a) -> (~a -> a) -> a
2		absurd	~a -> a -> ~(~a -> a)
3	2	a2i	(~a -> a) -> ~a -> ~(~a -> a)
4	3	a3d	(~a -> a) -> (~a -> a) -> a
5	1, 4	ax_mp	(~a -> a) -> a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)