Theorem neqfal ≪ | index | src | ≫

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

Step	Hyp	Ref	Expression
1		bitr4	(~a <-> F. <-> ~~a) -> (a <-> ~~a) -> (~a <-> F. <-> a)
2		eqfal	~a <-> F. <-> ~~a
3	1, 2	ax_mp	(a <-> ~~a) -> (~a <-> F. <-> a)
4		notnot	a <-> ~~a
5	3, 4	ax_mp	~a <-> F. <-> a

Axiom use

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