Theorem mtbir 671

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 132	. 2 ⊢ (𝜓 ↔ 𝜑)
4	1, 3	mtbi 670	1 ⊢ ¬ 𝜑

Syntax hints:  ¬ wn 3   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  850  nndc  851  fal  1360  ax-9  1531  nonconne  2359  nemtbir  2436  ru  2963  noel  3428  iun0  3945  0iun  3946  br0  4053  vprc  4137  iin0r  4171  nlim0  4396  snnex  4450  onsucelsucexmid  4531  0nelxp  4656  dm0  4843  iprc  4897  co02  5144  0fv  5552  frec0g  6400  nnsucuniel  6498  1nen2  6863  fidcenumlemrk  6955  djulclb  7056  ismkvnex  7155  pw1ne3  7231  sucpw1nel3  7234  3nsssucpw1  7237  0nnq  7365  0npr  7484  nqprdisj  7545  0ncn  7832  axpre-ltirr  7883  pnfnre  8001  mnfnre  8002  inelr  8543  xrltnr  9781  fzo0  10170  fzouzdisj  10182  inftonninf  10443  hashinfom  10760  3prm  12130  sqrt2irr  12164  ennnfonelem1  12410  bj-nndcALT  14549  bj-vprc  14687  pwle2  14787  exmidsbthrlem  14809