Theorem imbitrid

A mixed syllogism inference. (Contributed by NM, 12-Jan-1993.)

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