Theorem nbfal

Description: The negation of a proposition is equivalent to itself being equivalent to F. . (Contributed by Anthony Hart, 14-Aug-2011)

	Ref	Expression
Assertion	nbfal	$$⊢\neg \phi \leftrightarrow \left(\phi \leftrightarrow \perp \right)$$

Proof

Step	Hyp	Ref	Expression
1		fal	$$⊢\neg \perp$$
2	1	nbn	$$⊢\neg \phi \leftrightarrow \left(\phi \leftrightarrow \perp \right)$$