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	⊢ ( ¬ 𝜑 ↔ ( 𝜑 ↔ ⊥ ) )

Proof

Step	Hyp	Ref	Expression
1		fal	⊢ ¬ ⊥
2	1	nbn	⊢ ( ¬ 𝜑 ↔ ( 𝜑 ↔ ⊥ ) )