Theorem nbn2

The negation of a wff is equivalent to the wff's equivalence to falsehood. (Contributed by Juha Arpiainen, 19-Jan-2006.) (Proof shortened by Wolf Lammen, 28-Jan-2013.)

Conclusion
\( \vdash \neg \varphi \rightarrow (\neg \psi \leftrightarrow (\varphi \leftrightarrow \psi)) \)
Proof
l0
pm5.501
\( \vdash \neg \varphi \rightarrow (\neg \psi \leftrightarrow (\neg \varphi \leftrightarrow \neg \psi)) \)
notbi
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\neg \varphi \leftrightarrow \neg \psi) \)
bitr4di l0 _