Theorem syl5ibrcom

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

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