Theorem sylnbi

A mixed syllogism inference from a biconditional and an implication. Useful for substituting an antecedent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.)

Hypotheses
sylnbi.1
\( \vdash \varphi \leftrightarrow \psi \)
sylnbi.2
\( \vdash \neg \psi \rightarrow \chi \)
Conclusion
\( \vdash \neg \varphi \rightarrow \chi \)
Proof
sylnbi.1
l1
notbii _
\( \vdash \neg \varphi \leftrightarrow \neg \psi \)
sylnbi.2
\( \vdash \neg \psi \rightarrow \chi \)
sylbi l1 _