Theorem sylib

A mixed syllogism inference from an implication and a biconditional. (Contributed by NM, 3-Jan-1993.)

Hypotheses
sylib.1
\( \vdash \varphi \rightarrow \psi \)
sylib.2
\( \vdash \psi \leftrightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
l0
sylib.1
\( \vdash \varphi \rightarrow \psi \)
sylib.2
biimpi _
\( \vdash \psi \rightarrow \chi \)
syl l0 _