Theorem mtbir 675

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 674	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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  nnexmid  855  nndc  856  fal  1402  ax-9  1577  nonconne  2412  nemtbir  2489  ru  3027  noel  3495  iun0  4022  0iun  4023  br0  4132  vprc  4216  iin0r  4253  nlim0  4485  snnex  4539  onsucelsucexmid  4622  0nelxp  4747  dm0  4937  iprc  4993  co02  5242  0fv  5667  frec0g  6549  nnsucuniel  6649  1nen2  7030  1ndom2  7034  fidcenumlemrk  7132  djulclb  7233  ismkvnex  7333  pw1ne3  7426  sucpw1nel3  7429  3nsssucpw1  7432  0nnq  7562  0npr  7681  nqprdisj  7742  0ncn  8029  axpre-ltirr  8080  pnfnre  8199  mnfnre  8200  inelr  8742  xrltnr  9987  fzo0  10378  fzouzdisj  10390  inftonninf  10676  hashinfom  11012  lsw0  11132  3prm  12665  sqrt2irr  12699  ennnfonelem1  12993  bj-nndcALT  16177  bj-vprc  16314  pwle2  16423  exmidsbthrlem  16450