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 \phi$$
	mtbi.2	$$⊢\phi \leftrightarrow \psi$$
Assertion	mtbi	$$⊢\neg \psi$$

Proof

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