Theorem mtbir

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

	Ref	Expression
Hypotheses	mtbir.1	⊢ ¬ 𝜓
	mtbir.2	⊢ ( 𝜑 ↔ 𝜓 )
Assertion	mtbir	⊢ ¬ 𝜑

Proof

Step	Hyp	Ref	Expression
1		mtbir.1	⊢ ¬ 𝜓
2		mtbir.2	⊢ ( 𝜑 ↔ 𝜓 )
3	2	bicomi	⊢ ( 𝜓 ↔ 𝜑 )
4	1 3	mtbi	⊢ ¬ 𝜑