Metamath Proof Explorer

Theorem sylnibr

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

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


Step Hyp Ref Expression
1 sylnibr.1 φ ¬ ψ
2 sylnibr.2 χ ψ
3 2 bicomi ψ χ
4 1 3 sylnib φ ¬ χ