Theorem sylbid

A syllogism deduction. (Contributed by NM, 3-Aug-1994.)

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