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

Metamath Proof Explorer

Theorem mtbi

Description: An inference from a biconditional, related to modus tollens. (Contributed by NM, 15-Nov-1994) (Proof shortened by Wolf Lammen, 25-Oct-2012)

	Ref	Expression
Hypotheses	mtbi.1	$⊢ \neg φ$
	mtbi.2	$⊢ φ \leftrightarrow ψ$
Assertion	mtbi	$⊢ \neg ψ$

Proof

Step	Hyp	Ref	Expression
1		mtbi.1	$⊢ \neg φ$
2		mtbi.2	$⊢ φ \leftrightarrow ψ$
3	2	biimpri	$⊢ ψ \to φ$
4	1 3	mto	$⊢ \neg ψ$