Theorem imim12d

Deduction combining antecedents and consequents. Deduction associated with imim12 and imim12i. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mel L. O'Cat, 30-Oct-2011.)

Hypotheses
imim12d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
imim12d.2
\( \vdash \varphi \rightarrow \theta \rightarrow \tau \)
Conclusion
\( \vdash \varphi \rightarrow (\chi \rightarrow \theta) \rightarrow \psi \rightarrow \tau \)
Proof
l0
imim12d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
imim12d.2
imim2d _
\( \vdash \varphi \rightarrow (\chi \rightarrow \theta) \rightarrow \chi \rightarrow \tau \)
syl5d l0 _