Theorem excxor

This tautology shows that xor is really exclusive. (Contributed by FL, 22-Nov-2010.)

Conclusion
\( \vdash \varphi \veebar \psi \leftrightarrow \varphi \wedge \neg \psi \vee \neg \varphi \wedge \psi \)
Proof
l0
df-xor
\( \vdash \varphi \veebar \psi \leftrightarrow \neg (\varphi \leftrightarrow \psi) \)
l1
xor
\( \vdash \neg (\varphi \leftrightarrow \psi) \leftrightarrow \varphi \wedge \neg \psi \vee \psi \wedge \neg \varphi \)
ancom
orbi2i _
\( \vdash \varphi \wedge \neg \psi \vee \psi \wedge \neg \varphi \leftrightarrow \varphi \wedge \neg \psi \vee \neg \varphi \wedge \psi \)
3bitri l0 l1 _