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  7129  djulclb  7230  ismkvnex  7330  pw1ne3  7423  sucpw1nel3  7426  3nsssucpw1  7429  0nnq  7559  0npr  7678  nqprdisj  7739  0ncn  8026  axpre-ltirr  8077  pnfnre  8196  mnfnre  8197  inelr  8739  xrltnr  9983  fzo0  10374  fzouzdisj  10386  inftonninf  10672  hashinfom  11008  lsw0  11127  3prm  12658  sqrt2irr  12692  ennnfonelem1  12986  bj-nndcALT  16146  bj-vprc  16283  pwle2  16393  exmidsbthrlem  16420