Theorem nbbnOLD

Obsolete version of nbbn as of 10-Jun-2026. (Contributed by NM, 27-Jun-2002.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \neg \varphi \leftrightarrow \psi \leftrightarrow \neg (\varphi \leftrightarrow \psi) \)
Proof
l0
xor3
\( \vdash \neg (\varphi \leftrightarrow \psi) \leftrightarrow (\varphi \leftrightarrow \neg \psi) \)
l1
con2bi
\( \vdash \varphi \leftrightarrow \neg \psi \leftrightarrow (\psi \leftrightarrow \neg \varphi) \)
bicom
\( \vdash \psi \leftrightarrow \neg \varphi \leftrightarrow (\neg \varphi \leftrightarrow \psi) \)
3bitrri l0 l1 _