Theorem orim12i

Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.)

Hypotheses
orim12i.1
\( \vdash \varphi \rightarrow \psi \)
orim12i.2
\( \vdash \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \vee \chi \rightarrow \psi \vee \theta \)
Proof
orim12i.1
l1
orcd _
orim12i.2
olcd _
jaoi l1 _