This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	$⊢ φ \to \neg ψ$
	sylnibr.2	$⊢ χ \leftrightarrow ψ$
Assertion	sylnibr	$⊢ φ \to \neg χ$

Proof

Step	Hyp	Ref	Expression
1		sylnibr.1	$⊢ φ \to \neg ψ$
2		sylnibr.2	$⊢ χ \leftrightarrow ψ$
3	2	bicomi	$⊢ ψ \leftrightarrow χ$
4	1 3	sylnib	$⊢ φ \to \neg χ$