Theorem sylibr

A mixed syllogism inference from an implication and a biconditional. Useful for substituting a consequent with a definition. (Contributed by NM, 3-Jan-1993.)

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