Theorem orim1d

Disjoin antecedents and consequents in a deduction. (Contributed by NM, 23-Apr-1995.)

Hypothesis
orim1d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \vee \theta \rightarrow \chi \vee \theta \)
Proof
l0
orim1d.1
idd
orim12d l0 _