Theorem biimtrrdi

A mixed syllogism inference. (Contributed by NM, 18-May-1994.)

Hypotheses
biimtrrdi.1
\( \vdash \varphi \rightarrow (\chi \leftrightarrow \psi) \)
biimtrrdi.2
\( \vdash \chi \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \psi \rightarrow \theta \)
Proof
biimtrrdi.1
l1
biimprd _
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
biimtrrdi.2
\( \vdash \chi \rightarrow \theta \)
syl6 l1 _