Theorem sylbi

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

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