Theorem sylnibr

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

Hypotheses
sylnibr.1
\( \vdash \varphi \rightarrow \neg \psi \)
sylnibr.2
\( \vdash \chi \leftrightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \neg \chi \)
Proof
l0
sylnibr.1
\( \vdash \varphi \rightarrow \neg \psi \)
sylnibr.2
bicomi _
\( \vdash \psi \leftrightarrow \chi \)
sylnib l0 _