Theorem syl5ibcom

A mixed syllogism inference. (Contributed by NM, 19-Jun-2007.)

Hypotheses
imbitrid.1
\( \vdash \varphi \rightarrow \psi \)
imbitrid.2
\( \vdash \chi \rightarrow (\psi \leftrightarrow \theta) \)
Conclusion
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
Proof
l0
imbitrid.1
\( \vdash \varphi \rightarrow \psi \)
imbitrid.2
\( \vdash \chi \rightarrow (\psi \leftrightarrow \theta) \)
imbitrid l0 _
com12 _