Theorem mtbir 323

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

Syntax hints:  ¬ wn 3   ↔ wb 206

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 207

This theorem is referenced by:  3pm3.2ni  1487  fal  1551  eqneltri  2863  nemtbir  3044  ru  3802  ruOLD  3803  pssirr  4126  noel  4360  noelOLD  4361  iun0  5085  0iun  5086  br0  5215  vprc  5333  iin0  5380  nfnid  5393  opelopabsb  5549  0nelopab  5586  0nelxp  5734  0xp  5798  nrelv  5824  dm0  5945  cnv0  6172  co02  6291  nlim0  6454  snsn0non  6520  imadif  6662  0fv  6964  poxp2  8184  poseq  8199  tz7.44lem1  8461  nlim1  8545  nlim2  8546  sdom0  9174  canth2  9196  snnen2o  9300  1sdom2  9303  canthp1lem2  10722  pwxpndom2  10734  adderpq  11025  mulerpq  11026  0ncn  11202  ax1ne0  11229  inelr  12283  xrltnr  13182  fzouzdisj  13752  lsw0  14613  eirr  16253  ruc  16291  aleph1re  16293  sqrt2irr  16297  n2dvds1  16416  n2dvds3  16419  sadc0  16500  1nprm  16726  join0  18475  meet0  18476  smndex1n0mnd  18947  nsmndex1  18948  smndex2dnrinv  18950  odhash  19616  cnfldfun  21401  cnfldfunOLD  21414  zringndrg  21502  zfbas  23925  ustn0  24250  zclmncvs  25201  lhop  26075  dvrelog  26697  nosgnn0  27721  sltsolem1  27738  addsrid  28015  muls01  28156  mulsrid  28157  axlowdimlem13  28987  ntrl2v2e  30190  konigsberglem4  30287  avril1  30495  helloworld  30497  topnfbey  30501  vsfval  30665  dmadjrnb  31938  xrge00  32998  esumrnmpt2  34032  measvuni  34178  sibf0  34299  ballotlem4  34463  signswch  34538  satf0n0  35346  fmlaomn0  35358  gonan0  35360  goaln0  35361  fmla0disjsuc  35366  elpotr  35745  dfon2lem7  35753  linedegen  36107  nmotru  36374  limsucncmpi  36411  bj-ru1  36909  bj-0nel1  36919  bj-inftyexpitaudisj  37171  bj-pinftynminfty  37193  finxp0  37357  poimirlem30  37610  coss0  38435  epnsymrel  38518  diophren  42769  notbicom  45071  rexanuz2nf  45408  stoweidlem44  45965  fourierdlem62  46089  salexct2  46260  aisbnaxb  46826  dandysum2p2e4  46913  iota0ndef  46954  aiota0ndef  47012  257prm  47435  fmtno4nprmfac193  47448  139prmALT  47470  31prm  47471  127prm  47473  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  usgrexmpl2trifr  47852  0nodd  47893  2nodd  47895  1neven  47961  2zrngnring  47981  ex-gt  48820  alsi-no-surprise  48890