Theorem
xoror
Exclusive disjunction implies disjunction ("XOR implies OR"). (Contributed by BJ, 19-Apr-2019.)
Conclusion
\( \vdash \varphi \veebar \psi \rightarrow \varphi \vee \psi \)
Proof
xor2
\( \vdash \varphi \veebar \psi \leftrightarrow (\varphi \vee \psi) \wedge \neg (\varphi \wedge \psi) \)
simplbi
_
This is the content in the right pane.