Theorem imim12

Closed form of imim12i and of 3syl. (Contributed by BJ, 16-Jul-2019.)

Conclusion
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\chi \rightarrow \theta) \rightarrow (\psi \rightarrow \chi) \rightarrow \varphi \rightarrow \theta \)
Proof
l0
imim2
\( \vdash (\chi \rightarrow \theta) \rightarrow (\psi \rightarrow \chi) \rightarrow \psi \rightarrow \theta \)
imim1
\( \vdash (\varphi \rightarrow \psi) \rightarrow (\psi \rightarrow \theta) \rightarrow \varphi \rightarrow \theta \)
syl9r l0 _