Theorem
xornan2
XOR implies NAND (written with the
-/\
connector). (Contributed by BJ, 19-Apr-2019.)
Conclusion
\( \vdash \varphi \veebar \psi \rightarrow \varphi \barwedge \psi \)
Proof
l0
xornan
\( \vdash \varphi \veebar \psi \rightarrow \neg (\varphi \wedge \psi) \)
df-nan
\( \vdash \varphi \barwedge \psi \leftrightarrow \neg (\varphi \wedge \psi) \)
sylibr
l0
_
This is the content in the right pane.