Theorem orcanai

Change disjunction in consequent to conjunction in antecedent. (Contributed by NM, 8-Jun-1994.)

Hypothesis
orcanai.1
\( \vdash \varphi \rightarrow \psi \vee \chi \)
Conclusion
\( \vdash \varphi \wedge \neg \psi \rightarrow \chi \)
Proof
orcanai.1
ord _
imp _