Theorem notbid 318

Description: Deduction negating both sides of a logical equivalence. (Contributed by NM, 21-May-1994.)

Hypothesis

Ref	Expression
notbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
notbid	⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

Proof of Theorem notbid

Step	Hyp	Ref	Expression
1		notbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		notnotb 315	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
3		notnotb 315	. . 3 ⊢ (𝜒 ↔ ¬ ¬ 𝜒)
4	1, 2, 3	3bitr3g 313	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 ↔ ¬ ¬ 𝜒))
5	4	con4bid 317	1 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ 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:  notbi  319  annotanannot  835  con3ALT  1085  xorbi12d  1527  equsexvw  2007  cbvexvw  2039  cbvexdvaw  2041  excomimw  2046  hbe1w  2052  19.8aw  2054  exexw  2055  ru0  2133  cbvexv1  2347  cbvex2v  2349  drex1v  2375  cbvex  2404  cbvex2  2417  drex1  2446  eujustALT  2573  necon3abid  2969  neleq12d  3042  cbvrexdva  3218  cbvrexfw  3278  rexeqbidvvOLD  3308  cbvrexdva2  3320  cbvrexf  3332  cbvexeqsetf  3456  cgsex4gOLD  3489  ceqsex  3490  ceqsexv  3491  gencbval  3502  spcegf  3547  spc2gv  3555  spc2d  3557  spc3gv  3559  ceqsralbv  3612  cdeqnot  3727  rru  3738  ruOLD  3740  sbcng  3789  sbcrext  3824  cbvrexcsf  3893  difjust  3904  eldif  3912  dfpss3  4042  dfdif3OLD  4071  difeq2  4073  disjne  4408  pssdifcom1  4443  eldifpr  4616  rexsng  4634  elpwunsn  4642  eldiftp  4645  rexprg  4655  preqsnd  4816  disjxun  5097  nalset  5259  dtruALT2  5316  dtruALT  5334  rexxfrd  5355  rexxfr2d  5357  rexxfrd2  5359  rexxfr  5362  opthneg  5430  snopeqop  5455  otiunsndisj  5469  poeq1  5536  pocl  5541  swopo  5544  sotric  5563  sotrieq  5564  isso2i  5570  somo  5572  freq1  5592  frirr  5601  fr2nr  5602  frminex  5604  tz7.2  5608  wereu2  5622  poinxp  5706  frinxp  5708  posn  5711  frsn  5713  rexiunxp  5790  rexxpf  5797  intirr  6076  poirr2  6082  cnvpo  6246  dfpo2  6255  predpoirr  6292  predfrirr  6293  frpomin  6299  nordeq  6337  ordtri1  6351  ordtri3  6354  fvmpti  6941  fndmdif  6989  rexrnmptw  7042  rexrnmpt  7044  rexima  7186  f1imapss  7214  f1ounsn  7220  cbvexfo  7238  nf1const  7252  soisoi  7276  isopolem  7293  weniso  7302  imaeqsalvOLD  7312  canth  7314  riotaclb  7358  rexrnmpo  7500  ndmovg  7543  sorpssuni  7679  sorpssint  7680  fr3nr  7719  dfwe2  7721  ordsucsssuc  7767  nlimsucg  7786  orduninsuc  7787  dfom2  7812  ssnlim  7830  resf1extb  7878  f1oweALT  7918  frxp  8070  poxp  8072  frxp2  8088  frxp3  8095  xpord3inddlem  8098  soseq  8103  suppofssd  8147  suppcoss  8151  smoword  8300  tz7.48lem  8374  oacan  8477  oaword  8478  omlimcl  8507  omeulem1  8511  nnaword  8557  nnmword  8563  nneob  8586  naddss1  8619  brdifun  8668  swoer  8669  undifixp  8876  boxcutc  8883  2dom  8971  php  9135  phpeqd  9140  nndomog  9141  onomeneq  9142  nnsdomo  9147  unxpdomlem2  9161  frfi  9189  unfilem1  9209  tfsnfin2  9267  supeq3  9356  supeq123d  9357  supmo  9359  eqsup  9363  supub  9366  sup0  9374  suppr  9379  supisolem  9381  supisoex  9382  eqinf  9392  infval  9394  infmo  9404  infpr  9412  infempty  9416  oieq1  9421  ordtypecbv  9426  ordtypelem7  9433  wemapsolem  9459  canthwdom  9488  zfregcl  9503  zfregclOLD  9504  elirrv  9506  elirrvOLD  9507  elirr  9508  noinfep  9573  cantnfp1lem3  9593  ttrcltr  9629  rankr1clem  9736  carden2b  9883  domtri2  9905  alephord3  9992  alephdom2  10001  alephval3  10024  dfac9  10051  kmlem2  10066  kmlem4  10068  isfin4  10211  isfin7  10215  fin23lem11  10231  isf32lem5  10271  isf34lem4  10291  fin1a2lem6  10319  fin1a2lem7  10320  fin1a2lem12  10325  itunisuc  10333  ac6n  10399  zorn2g  10417  zornn0g  10419  ttukeylem7  10429  infinfg  10480  axpowndlem3  10514  axpowndlem4  10515  axregnd  10519  elgch  10537  engch  10543  fpwwe2lem12  10557  fpwwe2  10558  pwfseqlem1  10573  pwfseqlem3  10575  hargch  10588  addnidpi  10816  pinq  10842  nqereu  10844  ltsonq  10884  prlem934  10948  ltexprlem7  10957  addcanpr  10961  prlem936  10962  reclem2pr  10963  reclem3pr  10964  supexpr  10969  ltsosr  11009  supsrlem  11026  axpre-lttri  11080  axpre-sup  11084  xrlenlt  11201  axlttri  11208  axsup  11212  ltne  11234  dedekind  11300  readdcan  11311  leadd1  11609  ltsub1  11637  ltsub2  11638  leord1  11668  lediv1  12011  lemuldiv  12026  lerec  12029  le2msq  12046  infm3  12105  suprnub  12111  infregelb  12130  avgle1  12385  avgle2  12386  znnnlt1  12522  indstr  12833  zsupss  12854  uzsupss  12857  rpneg  12943  xralrple  13124  xleneg  13137  xltadd1  13175  xposdif  13181  xmulneg1  13188  xltmul1  13211  xrsupexmnf  13224  xrinfmexpnf  13225  xrsupsslem  13226  xrinfmsslem  13227  xrub  13231  supxrleub  13245  infxrgelb  13255  difreicc  13404  nn0disj  13564  nelfzo  13584  elfznelfzo  13693  fvinim0ffz  13709  injresinjlem  13710  ssnn0fi  13912  leexp2  14098  exp11nnd  14188  hashbnd  14263  hasheni  14275  hashfundm  14369  hashbc  14380  wrdsymb0  14476  swrdnd  14582  swrdnd2  14583  pfxnd0  14616  repswswrd  14711  repswccat  14713  cshwidxmod  14730  cnpart  15167  sqrtlt  15188  limsuplt  15406  rlimrege0  15506  isercoll  15595  efle  16047  odd2np1  16272  sumodd  16319  divalglem7  16330  ndvdsadd  16341  fldivndvdslt  16347  bitsfval  16354  bitsval  16355  bits0  16359  bitsp1  16362  bitsmod  16367  bitscmp  16369  bitsinv1lem  16372  sadadd2lem2  16381  saddisjlem  16395  bitsshft  16406  gcdneg  16453  algcvgblem  16508  lcmneg  16534  isprm3  16614  dvdsnprmd  16621  isprm5  16638  rpexp  16653  phiprmpw  16707  m1dvdsndvds  16730  pythagtrip  16766  pcgcd1  16809  prmpwdvds  16836  prmreclem2  16849  prmreclem3  16850  prmreclem5  16852  prmreclem6  16853  vdwlem6  16918  vdwnnlem2  16928  vdwnnlem3  16929  vdwnn  16930  prmlem0  17037  prmlem1a  17038  divsfval  17472  mrisval  17557  ismri  17558  ismri2dad  17564  cidpropd  17637  cat1lem  18024  plttr  18267  joinval  18302  meetval  18316  acsfiindd  18480  isnsgrp  18652  smndex1n0mnd  18841  mgm2nsgrplem2  18848  sgrp2nmndlem3  18854  symgpssefmnd  19329  symgfix2  19349  pmtrdifellem4  19412  psgnunilem1  19426  psgnunilem5  19427  psgnunilem2  19428  psgnunilem3  19429  pmtrsn  19452  sylow1lem3  19533  sylow2alem2  19551  efgsfo  19672  ablfac1eulem  20007  ablfac1eu  20008  pgpfac1lem1  20009  pgpfac1lem5  20014  nzrunit  20461  zrninitoringc  20613  islbs  21032  lbsind  21036  lbspss  21038  lbspropd  21055  lspsnne1  21076  islbs2  21113  lbsacsbs  21115  lbsextlem1  21117  lbsextlem3  21119  lbsextlem4  21120  lbsextg  21121  frlmlbs  21756  islindf  21771  islinds2  21772  islindf2  21773  lindfind  21775  lindsind  21776  lindfrn  21780  lindfmm  21786  lsslindf  21789  islindf4  21797  opsrtoslem2  22015  psdmul  22113  cply1coe0  22249  cply1coe0bi  22250  mdetunilem7  22566  mdetunilem8  22567  mdetunilem9  22568  maducoeval2  22588  pmatcollpw3fi1lem1  22734  fvmptnn04ifa  22798  fvmptnn04ifc  22800  fvmptnn04ifd  22801  chfacffsupp  22804  chfacfscmul0  22806  chfacfpmmul0  22810  elcls  23021  maxlp  23095  perfi  23103  ordtbaslem  23136  ordtval  23137  ordtbas2  23139  ordtopn1  23142  ordtopn2  23143  ordtcnv  23149  ordtrest  23150  ordtrest2lem  23151  ordtrest2  23152  pnfnei  23168  mnfnei  23169  isreg2  23325  ordthauslem  23331  cmpfi  23356  cmpfii  23357  bwth  23358  nconnsubb  23371  hausdiag  23593  txkgen  23600  kqdisj  23680  ordthmeolem  23749  fbfinnfr  23789  trfbas  23792  fbunfip  23817  fbasrn  23832  trfil3  23836  ufileu  23867  fin1aufil  23880  hausflim  23929  alexsubALTlem2  23996  alexsubALTlem3  23997  alexsubALTlem4  23998  ptcmplem2  24001  ptcmplem3  24002  stdbdbl  24465  iccntr  24770  reconnlem2  24776  iccpnfcnv  24902  xrhmeo  24904  lebnumlem1  24920  lebnumlem2  24921  lebnumlem3  24922  bcthlem4  25287  minveclem3b  25388  ivthlem2  25413  ivthlem3  25414  mbfmax  25610  mbfposr  25613  i1fd  25642  mbfi1fseqlem4  25679  itg2splitlem  25709  itg2monolem1  25711  itg2cnlem1  25722  dvne0  25976  lhop1lem  25978  deg1nn0clb  26055  dgrle  26208  coemulhi  26219  aaliou3lem9  26318  cos11  26502  logleb  26572  argrege0  26580  logdivle  26591  ellogdm  26608  cxple  26664  cxplt2  26667  cxple3  26670  isosctrlem1  26788  atandm  26846  atans2  26901  atantayl2  26908  eldmgm  26992  ftalem7  27049  isppw2  27085  musum  27161  dchrsum2  27239  bposlem1  27255  lgsmod  27294  lgsdir2lem2  27297  lgsdir2  27301  lgsne0  27306  lgsprme0  27310  gausslemma2dlem4  27340  lgsquadlem1  27351  2lgslem3  27375  2lgsoddprm  27387  2sq2  27404  addsqrexnreu  27413  rpvmasumlem  27458  padicabv  27601  ostth3  27609  ostth  27610  noextenddif  27640  nodenselem4  27659  nodenselem5  27660  nodenselem7  27662  nolt02o  27667  nogt01o  27668  noresle  27669  nosupprefixmo  27672  noinfprefixmo  27673  nosupcbv  27674  nosupdm  27676  nosupfv  27678  nosupres  27679  nosupbnd1lem1  27680  nosupbnd1lem3  27682  nosupbnd1lem5  27684  nosupbnd1  27686  nosupbnd2lem1  27687  nosupbnd2  27688  noinfcbv  27689  noinfdm  27691  noinffv  27693  noinfres  27694  noinfbnd1lem1  27695  noinfbnd1lem3  27697  noinfbnd1lem5  27699  noinfbnd1  27701  noinfbnd2lem1  27702  noinfbnd2  27703  lenlts  27724  ltsne  27746  nocvxminlem  27754  lesrec  27799  eqcuts3  27804  cuteq1  27817  newbday  27902  ltslpss  27908  cofcutr  27924  lrrecfr  27943  addsval  27962  ltadds2  27991  lenegs  28046  lesubsubsbd  28086  lesubsubs2bd  28087  lesubsubs3bd  28088  lesubaddsd  28093  ltmuls2  28171  lemuls2d  28174  lemuls1d  28175  oncutlt  28264  onles  28268  pw2cut2  28462  bdaypw2bnd  28465  bdayfinbndlem1  28467  istrkgld  28535  axtgupdim2  28547  tglowdim2l  28726  axlowdimlem16  29034  axlowdim2  29037  axlowdim  29038  numedglnl  29221  usgredg2v  29304  lfuhgr1v0e  29331  cusgrfi  29536  vtxd0nedgb  29566  vtxduhgr0edgnel  29572  1loopgrnb0  29580  1hevtxdg0  29583  vtxdgoddnumeven  29631  wlkp1lem1  29749  wlkp1lem2  29750  wlkp1lem5  29753  dfpth2  29806  crctcsh  29901  clwlkclwwlklem2a4  30076  eupth2eucrct  30296  eupth2lem3lem3  30309  eupth2lem3lem4  30310  eupth2lem3lem6  30312  eupth2lem3lem7  30313  eupth2lems  30317  eupth2  30318  konigsberglem4  30334  nfrgr2v  30351  frgrwopreglem3  30393  fusgr2wsp2nb  30413  frgrreggt1  30472  friendshipgt3  30477  lpni  30559  nmobndseqi  30858  minvecolem5  30960  chpsscon3  31582  chnle  31593  nonbooli  31730  pjnel  31805  specval  31977  nmcfnlbi  32131  stri  32336  hstri  32344  cvbr  32361  cvcon3  32363  chcv1  32434  cvexchlem  32447  chrelat2  32449  nelun  32591  elpreq  32606  nelpr  32609  ifeqeqx  32620  nfpconfp  32713  suppiniseg  32767  isoun  32783  suppss3  32804  xrge0infss  32842  infxrge0gelb  32848  eliccelico  32859  elicoelioo  32860  nndiffz1  32868  hashgt1  32890  expgt0b  32899  nn0min  32903  ccatws1f1o  33035  toslublem  33056  tosglblem  33058  pmtrcnel  33173  cycpmco2  33217  isarchi2  33269  archiabl  33282  elrgspnlem2  33327  elrgspnlem3  33328  0nellinds  33453  lindssn  33461  lindfpropd  33465  ssdifidlprm  33541  mxidlirred  33555  ssmxidl  33557  esplyind  33733  lbslsat  33775  lindsunlem  33783  rtelextdg2lem  33885  constrsqrtcl  33938  ordtcnvNEW  34079  ordtrestNEW  34080  ordtrest2NEWlem  34081  ordtrest2NEW  34082  ordtconnlem1  34083  xrge0iifcnv  34092  esumpcvgval  34237  esum2d  34252  ddemeas  34395  omssubadd  34459  oddpwdc  34513  eulerpartlems  34519  eulerpartlemf  34529  eulerpartlemt  34530  eulerpartlemr  34533  eulerpartlemgvv  34535  eulerpartlemn  34540  ballotlemfc0  34652  ballotlemfcc  34653  ballotlem4  34658  ballotlemimin  34665  ballotlem7  34695  plymulx  34707  signsply0  34710  reprinfz1  34781  reprpmtf1o  34785  reprdifc  34786  hgt750lema  34816  hgt750leme  34817  istrkg2d  34825  bnj23  34876  bnj1185  34951  bnj1228  35169  bnj1388  35191  bnj1417  35199  nummin  35251  axnulg  35266  fineqvnttrclselem1  35279  onvf1odlem2  35300  onvf1odlem3  35301  revwlk  35321  isacycgr  35341  acycgr0v  35344  prclisacycgr  35347  erdszelem10  35396  satf0n0  35574  fmlaomn0  35586  fmlasucdisj  35595  satfv1fvfmla1  35619  satefvfmla1  35621  ismfs  35745  mvtinf  35751  untelirr  35904  untsucf  35906  untangtr  35910  dfon2lem3  35979  dfon2lem4  35980  dfon2lem7  35983  dfon2lem9  35985  distel  35997  funpartfv  36141  dfrdg4  36147  nn0prpwlem  36518  nn0prpw  36519  limsucncmpi  36641  limsucncmp  36642  ordcmp  36643  weiunlem  36659  weiunfrlem  36660  weiunfr  36663  regsfromregtr  36670  regsfromsetind  36671  unblimceq0  36709  unbdqndv1  36710  bj-hbntbi  36907  bj-equsexvwd  36984  bj-cbvexdv  37003  bj-ru1  37146  bj-nuliota  37260  topdifinffinlem  37554  topdifinffin  37555  icorempo  37558  relowlpssretop  37571  finxpreclem2  37597  finxpreclem6  37603  wl-issetft  37789  wl-eujustlem1  37795  leceifl  37812  lindsadd  37816  lindsenlbs  37818  matunitlindflem1  37819  poimirlem16  37839  poimirlem17  37840  poimirlem18  37841  poimirlem19  37842  poimirlem21  37844  poimirlem23  37846  poimirlem26  37849  poimirlem27  37850  poimirlem28  37851  poimirlem31  37854  poimir  37856  mblfinlem2  37861  mblfinlem3  37862  ismblfin  37864  cnambfre  37871  itg2addnclem  37874  itg2addnclem2  37875  iblabsnclem  37886  ftc1anclem1  37896  areacirc  37916  heibor1lem  38012  heiborlem1  38014  heiborlem6  38019  heiborlem8  38021  heiborlem10  38023  smprngopr  38255  ecin0  38555  ax12inda  39276  riotaclbgBAD  39282  lcvfbr  39348  lcvbr  39349  lsatcv0  39359  l1cvpat  39382  opltcon3b  39532  cvrfval  39596  cvrval  39597  cvrnbtwn  39599  cvrval2  39602  cvrnbtwn2  39603  cvrnbtwn3  39604  cvrcon3b  39605  cvrnbtwn4  39607  atnlt  39641  iscvlat  39651  cvlexch1  39656  hlsuprexch  39709  hlrelat5N  39729  hlrelat2  39731  cvrval5  39743  3dimlem1  39786  3dim1lem5  39794  3dim2  39796  3dim3  39797  llnnlt  39851  islpln5  39863  lplni2  39865  lvolex3N  39866  lplnnle2at  39869  islpln2a  39876  lplnribN  39879  lplnexllnN  39892  lplnnlt  39893  lvoli3  39905  islvol5  39907  lvoli2  39909  lvolnle3at  39910  islvol2aN  39920  4atlem11  39937  lvolnltN  39946  dalawlem15  40213  4atexlemex2  40399  4atex  40404  4atex2-0aOLDN  40406  4atex2-0cOLDN  40408  lautcvr  40420  ltrnfset  40445  ltrnset  40446  ltrnu  40449  trlfset  40488  trlset  40489  trlval2  40491  cdlemd6  40531  cdleme0nex  40618  cdleme18d  40623  cdleme25b  40682  cdleme25cv  40686  cdleme29b  40703  cdleme31fv  40718  cdleme31fv2  40721  cdlemefrs29bpre0  40724  cdlemefr32sn2aw  40732  cdlemefr29bpre0N  40734  cdlemefr29clN  40735  cdlemefr32fvaN  40737  cdlemefr32fva1  40738  cdlemefs32sn1aw  40742  cdleme32fva  40765  cdleme32fvaw  40767  cdleme40v  40797  cdleme42b  40806  cdleme46f2g2  40821  cdleme46f2g1  40822  cdleme48gfv  40865  cdlemg1fvawlemN  40901  cdlemg1cex  40916  cdlemg6d  40949  cdlemm10N  41446  dicffval  41502  dicfval  41503  dicval  41504  dicfnN  41511  dicvalrelN  41513  dihffval  41558  dihfval  41559  dihlsscpre  41562  dvh4dimat  41766  dvh3dimatN  41767  dvh4dimlem  41771  dvh3dim  41774  dvh4dimN  41775  dvh3dim2  41776  dvh3dim3N  41777  mapdcv  41988  mapdh9aOLDN  42118  hdmapfval  42155  hdmapval  42156  hdmapval2  42160  hdmap11lem2  42170  dvrelog2b  42388  aks4d1p4  42401  aks4d1p5  42402  aks4d1p7  42405  aks4d1p8d2  42407  aks4d1p8  42409  aks4d1  42411  aks6d1c2p2  42441  hashnexinj  42450  rspcsbnea  42453  aks6d1c5  42461  aks6d1c6lem3  42494  aks6d1c7  42506  supinf  42564  oexpreposd  42644  mullt0b2d  42806  flt4lem7  42969  nna4b4nsq  42970  ellz1  43076  rencldnfilem  43129  jm2.22  43304  jm2.23  43305  wepwsolem  43351  fnwe2lem2  43360  aomclem8  43370  unxpwdom3  43404  onsupmaxb  43548  onexlimgt  43552  onsupeqnmax  43556  onov0suclim  43583  oaordnr  43605  omnord1  43614  oenord1  43625  oaomoencom  43626  oenass  43628  cantnfresb  43633  tfsnfin  43661  ralopabb  43719  nlimsuc  43749  ifpbi12  43796  dfsucon  43831  sqrtcvallem1  43939  ss2iundf  43967  frege124d  44069  clsk3nimkb  44348  clsk1indlem1  44353  clsk1independent  44354  ntrneineine1lem  44392  ntrneicls11  44398  clsneiel1  44416  clsneiel2  44417  neicvgel1  44427  neicvgel2  44428  radcnvrat  44622  rusbcALT  44746  en3lpVD  45152  0elaxnul  45291  omssaxinf2  45296  permaxnul  45316  permaxinf2lem  45320  nregmodel  45325  eliin2f  45415  nssd  45416  wessf1ornlem  45496  rexanuz2nf  45803  limsupre2lem  46035  icccncfext  46198  stoweidlem14  46325  stoweidlem34  46345  stoweidlem59  46370  etransclem24  46569  nnfoctbdjlem  46766  nnfoctbdj  46767  hspmbllem2  46938  nsssmfmbflem  47089  fsetsnprcnex  47368  eu2ndop1stv  47438  afvfv0bi  47465  afvco2  47489  ndmaovg  47497  ndfatafv2nrn  47534  afv2ndefb  47537  afv2fv0  47578  nelbr  47587  otiunsndisjX  47592  fun2dmnopgexmpl  47597  ltnltne  47612  readdcnnred  47616  resubcnnred  47617  recnmulnred  47618  cndivrenred  47619  ichnreuop  47785  fmtnoinf  47849  odz2prm2pw  47876  prmdvdsfmtnof1lem2  47898  lighneallem3  47920  lighneallem4  47923  requad1  47935  isodd3  47965  bits0ALTV  47992  nfermltl8rev  48055  nfermltl2rev  48056  nfermltlrev  48057  upgrimpths  48222  isubgr3stgrlem3  48281  usgrexmpl12ngric  48351  pgnbgreunbgrlem2lem1  48427  pgnbgreunbgrlem2lem2  48428  pgnbgreunbgrlem2lem3  48429  pgnbgreunbgrlem5lem1  48433  pgnbgreunbgrlem5lem2  48434  pgnbgreunbgrlem5lem3  48435  lgricngricex  48442  lidldomnnring  48549  ztprmneprm  48660  lindepsnlininds  48765  islindeps  48766  lindslinindsimp2lem5  48775  lindslinindsimp2  48776  line2ylem  49064  line2xlem  49066  map0cor  49167  nelsubc3lem  49382  fulltermc2  49824  setc1onsubc  49914  cnelsubclem  49915  elsetrecslem  50011