Theorem imorri

Infer implication from disjunction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

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