Theorem orim12d

Disjoin antecedents and consequents in a deduction. See orim12dALT for a proof which does not depend on [df-an]. (Contributed by NM, 10-May-1994.)

Hypotheses
orim12d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
orim12d.2
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow \psi \vee \theta \rightarrow \chi \vee \tau \)
Proof
l0
orim12d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
l1
orim12d.2
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
pm3.48
\( \vdash (\psi \rightarrow \chi) \wedge (\theta \rightarrow \tau) \rightarrow \psi \vee \theta \rightarrow \chi \vee \tau \)
syl2anc l0 l1 _