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  4021  0iun  4022  br0  4131  vprc  4215  iin0r  4252  nlim0  4484  snnex  4538  onsucelsucexmid  4621  0nelxp  4746  dm0  4936  iprc  4992  co02  5241  0fv  5664  frec0g  6541  nnsucuniel  6639  1nen2  7018  1ndom2  7022  fidcenumlemrk  7117  djulclb  7218  ismkvnex  7318  pw1ne3  7411  sucpw1nel3  7414  3nsssucpw1  7417  0nnq  7547  0npr  7666  nqprdisj  7727  0ncn  8014  axpre-ltirr  8065  pnfnre  8184  mnfnre  8185  inelr  8727  xrltnr  9971  fzo0  10362  fzouzdisj  10374  inftonninf  10659  hashinfom  10995  lsw0  11114  3prm  12645  sqrt2irr  12679  ennnfonelem1  12973  bj-nndcALT  16080  bj-vprc  16217  pwle2  16323  exmidsbthrlem  16349