Theorem inot ≪ | index | src | ≫

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

Step	Hyp	Ref	Expression
1		contra	(~~a -> ~a) -> ~a
2		imim1	(~~a -> a) -> (a -> ~a) -> ~~a -> ~a
3		dne	~~a -> a
4	2, 3	ax_mp	(a -> ~a) -> ~~a -> ~a
5	1, 4	syl	(a -> ~a) -> ~a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp)