Metamath Proof Explorer

Theorem sylnbi

Description: 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)

Ref Expression
Hypotheses sylnbi.1 φ ψ
sylnbi.2 ¬ ψ χ
Assertion sylnbi ¬ φ χ


Step Hyp Ref Expression
1 sylnbi.1 φ ψ
2 sylnbi.2 ¬ ψ χ
3 1 notbii ¬ φ ¬ ψ
4 3 2 sylbi ¬ φ χ