Theorem imbitrrid

A mixed syllogism inference. (Contributed by NM, 3-Apr-1994.)

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