Theorem biimtrdi

A mixed syllogism inference. (Contributed by NM, 2-Jan-1994.)

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