Theorem sylibrd

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

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