Theorem mtbir 326

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

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  3pm3.2ni  1519  fal  1584  eqneltri  2879  nemtbir  3051  ru  3738  pssirrOLD  4052  noel  4284  vn0  4291  vn0OLD  4292  uni0  4896  iun0  5020  0iun  5021  br0  5154  vprcOLD  5278  iin0  5327  nfnid  5340  opelopabsb  5508  0nelopab  5544  0nelxp  5689  nrelvOLD  5781  cnv0  5863  cnv0OLD  5864  dm0  5904  co02  6257  nlim0  6418  snsn0non  6484  imadif  6618  0fv  6920  poxp2  8142  poseq  8157  tz7.44lem1  8395  nlim1  8479  nlim2  8480  sdom0  9110  canth2  9131  snnen2o  9218  1sdom2  9221  canthp1lem2  10665  pwxpndom2  10677  adderpq  10968  mulerpq  10969  0ncn  11145  ax1ne0  11172  inelr  12235  xrltnr  13173  fzouzdisj  13754  lsw0  14633  eirr  16296  ruc  16334  aleph1re  16336  sqrt2irr  16340  n2dvds1  16461  n2dvds3  16464  sadc0  16547  1nprm  16772  join0  18494  meet0  18495  smndex1n0mnd  19027  nsmndex1  19028  smndex2dnrinv  19030  degenmgmnfn  19052  degenmgm2nfun  19055  odhash  19704  cnfldfun  21602  zringndrg  21684  zfbas  24125  ustn0  24450  zclmncvs  25379  lhop  26246  dvrelog  26877  nosgnn0  27897  ltssolem1  27914  addsrid  28232  muls01  28380  mulsrid  28381  axlowdimlem13  29414  ntrl2v2e  30641  konigsberglem4  30738  avril1  30946  helloworld  30948  topnfbey  30952  nowisdomv  30957  vsfval  31117  dmadjrnb  32390  xrge00  33457  domnprodeq0  33722  esumrnmpt2  34581  measvuni  34728  sibf0  34848  ballotlem4  35013  signswch  35072  satf0n0  35960  fmlaomn0  35972  gonan0  35974  goaln0  35975  fmla0disjsuc  35980  elpotr  36361  dfon2lem7  36369  linedegen  36726  nmotru  37030  limsucncmpi  37067  mh-inf3sn  37164  bj-ru1  37690  bj-0nel1  37700  bj-inftyexpitaudisj  37960  bj-pinftynminfty  37982  finxp0  38148  poimirlem30  38402  coss0  39320  epnsymrel  39397  sn-inelr  43378  diophren  43657  permaxnul  45834  permaxinf2lem  45838  notbicom  46000  rexanuz2nf  46323  stoweidlem44  46875  fourierdlem62  46999  salexct2  47170  chnerlem1  47713  aisbnaxb  47802  dandysum2p2e4  47889  iota0ndef  47930  aiota0ndef  47988  257prm  48467  fmtno4nprmfac193  48480  139prmALT  48502  31prm  48503  127prm  48505  nnsum4primeseven  48719  nnsum4primesevenALTV  48720  usgrexmpl2trifr  48956  0nodd  49088  2nodd  49090  1neven  49156  2zrngnring  49176  ex-gt  50657  als-no-surprise  50738  rals-no-surprise  50739