Theorem xor2

Two ways to express "exclusive or". (Contributed by Mario Carneiro, 4-Sep-2016.)

Conclusion
\( \vdash \varphi \veebar \psi \leftrightarrow (\varphi \vee \psi) \wedge \neg (\varphi \wedge \psi) \)
Proof
l0
df-xor
\( \vdash \varphi \veebar \psi \leftrightarrow \neg (\varphi \leftrightarrow \psi) \)
nbi2
\( \vdash \neg (\varphi \leftrightarrow \psi) \leftrightarrow (\varphi \vee \psi) \wedge \neg (\varphi \wedge \psi) \)
bitri l0 _