Theorem nbior

If two propositions are not equivalent, then at least one is true. (Contributed by BJ, 19-Apr-2019.) (Proof shortened by Wolf Lammen, 19-Jan-2020.)

Conclusion
\( \vdash \neg (\varphi \leftrightarrow \psi) \rightarrow \varphi \vee \psi \)
Proof
norbi
con1i _