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  2880  nemtbir  3052  ru  3738  pssirrOLD  4052  noel  4284  vn0  4291  vn0OLD  4292  uni0  4896  iun0  5020  0iun  5021  br0  5154  vprcOLD  5275  iin0  5324  nfnid  5337  opelopabsb  5504  0nelopab  5540  0nelxp  5685  nrelvOLD  5778  cnv0  5861  cnv0OLD  5862  dm0  5902  co02  6255  nlim0  6416  snsn0non  6482  imadif  6616  0fv  6918  poxp2  8144  poseq  8159  tz7.44lem1  8397  nlim1  8481  nlim2  8482  sdom0  9112  canth2  9133  snnen2o  9220  1sdom2  9223  canthp1lem2  10719  pwxpndom2  10731  adderpq  11022  mulerpq  11023  0ncn  11199  ax1ne0  11226  inelr  12291  xrltnr  13229  fzouzdisj  13810  lsw0  14690  eirr  16353  ruc  16391  aleph1re  16393  sqrt2irr  16397  n2dvds1  16518  n2dvds3  16521  sadc0  16604  1nprm  16834  join0  18557  meet0  18558  smndex1n0mnd  19091  nsmndex1  19092  smndex2dnrinv  19094  degenmgmnfn  19116  degenmgm2nfun  19119  odhash  19768  cnfldfun  21672  zringndrg  21754  zfbas  24195  ustn0  24520  zclmncvs  25449  lhop  26316  dvrelog  26947  nosgnn0  27997  ltssolem1  28014  addsrid  28332  muls01  28480  mulsrid  28481  axlowdimlem13  29514  ntrl2v2e  30741  konigsberglem4  30838  avril1  31046  helloworld  31048  topnfbey  31052  nowisdomv  31057  vsfval  31217  dmadjrnb  32490  xrge00  33557  domnprodeq0  33822  esumrnmpt2  34682  measvuni  34829  sibf0  34949  ballotlem4  35114  signswch  35173  satf0n0  36112  fmlaomn0  36124  gonan0  36126  goaln0  36127  fmla0disjsuc  36132  elpotr  36513  dfon2lem7  36521  linedegen  36878  nmotru  37166  limsucncmpi  37203  mh-inf3sn  37300  bj-ru1  37826  bj-0nel1  37836  bj-inftyexpitaudisj  38094  bj-pinftynminfty  38116  finxp0  38282  poimirlem30  38536  coss0  39469  epnsymrel  39546  sn-inelr  43519  diophren  43773  permaxnul  45950  permaxinf2lem  45954  notbicom  46123  rexanuz2nf  46446  stoweidlem44  46998  fourierdlem62  47122  salexct2  47293  chnerlem1  47836  aisbnaxb  47925  dandysum2p2e4  48012  iota0ndef  48053  aiota0ndef  48111  257prm  48590  fmtno4nprmfac193  48603  139prmALT  48625  31prm  48626  127prm  48628  nnsum4primeseven  48842  nnsum4primesevenALTV  48843  usgrexmpl2trifr  49079  0nodd  49211  2nodd  49213  1neven  49279  2zrngnring  49299  ex-gt  50765  als-no-surprise  50846  rals-no-surprise  50847