Theorem sylibd

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

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