Theorem imim12i

Inference joining two implications. Inference associated with imim12. Its associated inference is 3syl. (Contributed by NM, 12-Mar-1993.) (Proof shortened by Mel L. O'Cat, 29-Oct-2011.)

Hypotheses
imim12i.1
\( \vdash \varphi \rightarrow \psi \)
imim12i.2
\( \vdash \chi \rightarrow \theta \)
Conclusion
\( \vdash (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \theta \)
Proof
l0
imim12i.1
\( \vdash \varphi \rightarrow \psi \)
imim12i.2
imim2i _
\( \vdash (\psi \rightarrow \chi) \rightarrow \psi \rightarrow \theta \)
syl5 l0 _