Theorem orrd

Deduce disjunction from implication. (Contributed by NM, 27-Nov-1995.)

Hypothesis
orrd.1
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \vee \chi \)
Proof
l0
orrd.1
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \chi \)
pm2.54
\( \vdash (\neg \psi \rightarrow \chi) \rightarrow \psi \vee \chi \)
syl l0 _