Theorem xornan

Exclusive disjunction implies alternative denial ("XOR implies NAND"). (Contributed by BJ, 19-Apr-2019.)

Conclusion
\( \vdash \varphi \veebar \psi \rightarrow \neg (\varphi \wedge \psi) \)
Proof
xor2
\( \vdash \varphi \veebar \psi \leftrightarrow (\varphi \vee \psi) \wedge \neg (\varphi \wedge \psi) \)
simprbi _