Theorem nbn

The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 3-Oct-2013.)

Hypothesis
nbn.1
\( \vdash \neg \varphi \)
Conclusion
\( \vdash \neg \psi \leftrightarrow (\psi \leftrightarrow \varphi) \)
Proof
l0
nbn.1
\( \vdash \neg \varphi \)
bibif
\( \vdash \neg \varphi \rightarrow (\psi \leftrightarrow \varphi \leftrightarrow \neg \psi) \)
ax-mp l0 _
bicomi _