Theorem ori

Infer implication from disjunction. (Contributed by NM, 11-Jun-1994.)

Hypothesis
ori.1
\( \vdash \varphi \vee \psi \)
Conclusion
\( \vdash \neg \varphi \rightarrow \psi \)
Proof
l0
ori.1
\( \vdash \varphi \vee \psi \)
df-or
\( \vdash \varphi \vee \psi \leftrightarrow \neg \varphi \rightarrow \psi \)
mpbi l0 _