Theorem mtbir 290

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

Hypotheses

Ref	Expression
mtbir.1	⊢ ¬ ψ
mtbir.2	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
mtbir	⊢ ¬ φ

Proof of Theorem mtbir

Step	Hyp	Ref	Expression
1		mtbir.1	. 2 ⊢ ¬ ψ
2		mtbir.2	. . 3 ⊢ (φ ↔ ψ)
3	2	bicomi 193	. 2 ⊢ (ψ ↔ φ)
4	1, 3	mtbi 289	1 ⊢ ¬ φ

Syntax hints:  ¬ wn 3   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  fal  1322  nonconne  2524  nemtbir  2605  ru  3046  pssirr  3370  indifdir  3512  necompl  3545  noel  3555  npss0  3590  iun0  4023  0iun  4024  0nel1c  4160  0nelsuc  4401  nndisjeq  4430  addcnul1  4453  eqtfinrelk  4487  nulnnn  4557  0cnelphi  4598  dm0  4919  cnv0  5032  co02  5093  co01  5094  nfunv  5139  imadif  5172  fv01  5355  1p1e2c  6156  2p1e3c  6157  fnfreclem2  6319