Theorem nbi2

Two ways to express "exclusive or". (Contributed by NM, 3-Jan-2005.) (Proof shortened by Wolf Lammen, 24-Jan-2013.)

Conclusion
\( \vdash \neg (\varphi \leftrightarrow \psi) \leftrightarrow (\varphi \vee \psi) \wedge \neg (\varphi \wedge \psi) \)
Proof
l0
xor3
\( \vdash \neg (\varphi \leftrightarrow \psi) \leftrightarrow (\varphi \leftrightarrow \neg \psi) \)
pm5.17
\( \vdash (\varphi \vee \psi) \wedge \neg (\varphi \wedge \psi) \leftrightarrow (\varphi \leftrightarrow \neg \psi) \)
bitr4i l0 _