Theorem ord

Deduce implication from disjunction. (Contributed by NM, 18-May-1994.)

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