Theorem imfal ≪ | index | src | ≫

theorem imfal (a: wff): $ a -> F. <-> ~a $;

Step	Hyp	Ref	Expression
1		notfal	~F.
2		con3	(a -> F.) -> ~F. -> ~a
3	1, 2	mpi	(a -> F.) -> ~a
4		absurd	~a -> a -> F.
5	3, 4	ibii	a -> F. <-> ~a

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru)