Theorem nbbn

Move negation outside of biconditional. Compare Theorem *5.18 of [WhiteheadRussell] p. 124. (Contributed by NM, 27-Jun-2002.) (Proof shortened by Wolf Lammen, 20-Sep-2013.) (Proof shortened by Umit Teoman Dogan, 10-Jun-2026.)

Conclusion
\( \vdash \neg \varphi \leftrightarrow \psi \leftrightarrow \neg (\varphi \leftrightarrow \psi) \)
Proof
l0
pm5.18
\( \vdash \neg \varphi \leftrightarrow \psi \leftrightarrow \neg (\neg \varphi \leftrightarrow \neg \psi) \)
notbi
\( \vdash \varphi \leftrightarrow \psi \leftrightarrow (\neg \varphi \leftrightarrow \neg \psi) \)
xchbinxr l0 _