Theorem sylbird

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

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