Theorem imori

Infer disjunction from implication. (Contributed by NM, 12-Mar-2012.)

Hypothesis
imori.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \neg \varphi \vee \psi \)
Proof
l0
imori.1
\( \vdash \varphi \rightarrow \psi \)
imor
\( \vdash \varphi \rightarrow \psi \leftrightarrow \neg \varphi \vee \psi \)
mpbi l0 _