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  3219  cbvrexfw  3279  rexeqbidvvOLD  3309  cbvrexdva2  3321  cbvrexf  3333  cbvexeqsetf  3457  cgsex4gOLD  3490  ceqsex  3491  ceqsexv  3492  gencbval  3503  spcegf  3548  spc2gv  3556  spc2d  3558  spc3gv  3560  ceqsralbv  3613  cdeqnot  3728  rru  3739  ruOLD  3741  sbcng  3790  sbcrext  3825  cbvrexcsf  3894  difjust  3905  eldif  3913  dfpss3  4043  dfdif3OLD  4072  difeq2  4074  disjne  4409  pssdifcom1  4444  eldifpr  4617  rexsng  4635  elpwunsn  4643  eldiftp  4646  rexprg  4656  preqsnd  4817  disjxun  5098  nalset  5262  dtruALT2  5319  dtruALT  5337  rexxfrd  5358  rexxfr2d  5360  rexxfrd2  5362  rexxfr  5365  opthneg  5439  snopeqop  5464  otiunsndisj  5478  poeq1  5545  pocl  5550  swopo  5553  sotric  5572  sotrieq  5573  isso2i  5579  somo  5581  freq1  5601  frirr  5610  fr2nr  5611  frminex  5613  tz7.2  5617  wereu2  5631  poinxp  5715  frinxp  5717  posn  5720  frsn  5722  rexiunxp  5799  rexxpf  5806  intirr  6085  poirr2  6091  cnvpo  6255  dfpo2  6264  predpoirr  6301  predfrirr  6302  frpomin  6308  nordeq  6346  ordtri1  6360  ordtri3  6363  fvmpti  6950  fndmdif  6998  rexrnmptw  7051  rexrnmpt  7053  rexima  7196  f1imapss  7224  f1ounsn  7230  cbvexfo  7248  nf1const  7262  soisoi  7286  isopolem  7303  weniso  7312  imaeqsalvOLD  7322  canth  7324  riotaclb  7368  rexrnmpo  7510  ndmovg  7553  sorpssuni  7689  sorpssint  7690  fr3nr  7729  dfwe2  7731  ordsucsssuc  7777  nlimsucg  7796  orduninsuc  7797  dfom2  7822  ssnlim  7840  resf1extb  7888  f1oweALT  7928  frxp  8080  poxp  8082  frxp2  8098  frxp3  8105  xpord3inddlem  8108  soseq  8113  suppofssd  8157  suppcoss  8161  smoword  8310  tz7.48lem  8384  oacan  8487  oaword  8488  omlimcl  8517  omeulem1  8521  nnaword  8567  nnmword  8573  nneob  8596  naddss1  8629  brdifun  8678  swoer  8679  undifixp  8886  boxcutc  8893  2dom  8981  php  9145  phpeqd  9150  nndomog  9151  onomeneq  9152  nnsdomo  9157  unxpdomlem2  9171  frfi  9199  unfilem1  9219  tfsnfin2  9277  supeq3  9366  supeq123d  9367  supmo  9369  eqsup  9373  supub  9376  sup0  9384  suppr  9389  supisolem  9391  supisoex  9392  eqinf  9402  infval  9404  infmo  9414  infpr  9422  infempty  9426  oieq1  9431  ordtypecbv  9436  ordtypelem7  9443  wemapsolem  9469  canthwdom  9498  zfregcl  9513  zfregclOLD  9514  elirrv  9516  elirrvOLD  9517  elirr  9518  noinfep  9583  cantnfp1lem3  9603  ttrcltr  9639  rankr1clem  9746  carden2b  9893  domtri2  9915  alephord3  10002  alephdom2  10011  alephval3  10034  dfac9  10061  kmlem2  10076  kmlem4  10078  isfin4  10221  isfin7  10225  fin23lem11  10241  isf32lem5  10281  isf34lem4  10301  fin1a2lem6  10329  fin1a2lem7  10330  fin1a2lem12  10335  itunisuc  10343  ac6n  10409  zorn2g  10427  zornn0g  10429  ttukeylem7  10439  infinfg  10490  axpowndlem3  10524  axpowndlem4  10525  axregnd  10529  elgch  10547  engch  10553  fpwwe2lem12  10567  fpwwe2  10568  pwfseqlem1  10583  pwfseqlem3  10585  hargch  10598  addnidpi  10826  pinq  10852  nqereu  10854  ltsonq  10894  prlem934  10958  ltexprlem7  10967  addcanpr  10971  prlem936  10972  reclem2pr  10973  reclem3pr  10974  supexpr  10979  ltsosr  11019  supsrlem  11036  axpre-lttri  11090  axpre-sup  11094  xrlenlt  11211  axlttri  11218  axsup  11222  ltne  11244  dedekind  11310  readdcan  11321  leadd1  11619  ltsub1  11647  ltsub2  11648  leord1  11678  lediv1  12021  lemuldiv  12036  lerec  12039  le2msq  12056  infm3  12115  suprnub  12121  infregelb  12140  avgle1  12395  avgle2  12396  znnnlt1  12532  indstr  12843  zsupss  12864  uzsupss  12867  rpneg  12953  xralrple  13134  xleneg  13147  xltadd1  13185  xposdif  13191  xmulneg1  13198  xltmul1  13221  xrsupexmnf  13234  xrinfmexpnf  13235  xrsupsslem  13236  xrinfmsslem  13237  xrub  13241  supxrleub  13255  infxrgelb  13265  difreicc  13414  nn0disj  13574  nelfzo  13594  elfznelfzo  13703  fvinim0ffz  13719  injresinjlem  13720  ssnn0fi  13922  leexp2  14108  exp11nnd  14198  hashbnd  14273  hasheni  14285  hashfundm  14379  hashbc  14390  wrdsymb0  14486  swrdnd  14592  swrdnd2  14593  pfxnd0  14626  repswswrd  14721  repswccat  14723  cshwidxmod  14740  cnpart  15177  sqrtlt  15198  limsuplt  15416  rlimrege0  15516  isercoll  15605  efle  16057  odd2np1  16282  sumodd  16329  divalglem7  16340  ndvdsadd  16351  fldivndvdslt  16357  bitsfval  16364  bitsval  16365  bits0  16369  bitsp1  16372  bitsmod  16377  bitscmp  16379  bitsinv1lem  16382  sadadd2lem2  16391  saddisjlem  16405  bitsshft  16416  gcdneg  16463  algcvgblem  16518  lcmneg  16544  isprm3  16624  dvdsnprmd  16631  isprm5  16648  rpexp  16663  phiprmpw  16717  m1dvdsndvds  16740  pythagtrip  16776  pcgcd1  16819  prmpwdvds  16846  prmreclem2  16859  prmreclem3  16860  prmreclem5  16862  prmreclem6  16863  vdwlem6  16928  vdwnnlem2  16938  vdwnnlem3  16939  vdwnn  16940  prmlem0  17047  prmlem1a  17048  divsfval  17482  mrisval  17567  ismri  17568  ismri2dad  17574  cidpropd  17647  cat1lem  18034  plttr  18277  joinval  18312  meetval  18326  acsfiindd  18490  isnsgrp  18662  smndex1n0mnd  18854  mgm2nsgrplem2  18861  sgrp2nmndlem3  18867  symgpssefmnd  19342  symgfix2  19362  pmtrdifellem4  19425  psgnunilem1  19439  psgnunilem5  19440  psgnunilem2  19441  psgnunilem3  19442  pmtrsn  19465  sylow1lem3  19546  sylow2alem2  19564  efgsfo  19685  ablfac1eulem  20020  ablfac1eu  20021  pgpfac1lem1  20022  pgpfac1lem5  20027  nzrunit  20474  zrninitoringc  20626  islbs  21045  lbsind  21049  lbspss  21051  lbspropd  21068  lspsnne1  21089  islbs2  21126  lbsacsbs  21128  lbsextlem1  21130  lbsextlem3  21132  lbsextlem4  21133  lbsextg  21134  frlmlbs  21769  islindf  21784  islinds2  21785  islindf2  21786  lindfind  21788  lindsind  21789  lindfrn  21793  lindfmm  21799  lsslindf  21802  islindf4  21810  opsrtoslem2  22028  psdmul  22126  cply1coe0  22262  cply1coe0bi  22263  mdetunilem7  22579  mdetunilem8  22580  mdetunilem9  22581  maducoeval2  22601  pmatcollpw3fi1lem1  22747  fvmptnn04ifa  22811  fvmptnn04ifc  22813  fvmptnn04ifd  22814  chfacffsupp  22817  chfacfscmul0  22819  chfacfpmmul0  22823  elcls  23034  maxlp  23108  perfi  23116  ordtbaslem  23149  ordtval  23150  ordtbas2  23152  ordtopn1  23155  ordtopn2  23156  ordtcnv  23162  ordtrest  23163  ordtrest2lem  23164  ordtrest2  23165  pnfnei  23181  mnfnei  23182  isreg2  23338  ordthauslem  23344  cmpfi  23369  cmpfii  23370  bwth  23371  nconnsubb  23384  hausdiag  23606  txkgen  23613  kqdisj  23693  ordthmeolem  23762  fbfinnfr  23802  trfbas  23805  fbunfip  23830  fbasrn  23845  trfil3  23849  ufileu  23880  fin1aufil  23893  hausflim  23942  alexsubALTlem2  24009  alexsubALTlem3  24010  alexsubALTlem4  24011  ptcmplem2  24014  ptcmplem3  24015  stdbdbl  24478  iccntr  24783  reconnlem2  24789  iccpnfcnv  24915  xrhmeo  24917  lebnumlem1  24933  lebnumlem2  24934  lebnumlem3  24935  bcthlem4  25300  minveclem3b  25401  ivthlem2  25426  ivthlem3  25427  mbfmax  25623  mbfposr  25626  i1fd  25655  mbfi1fseqlem4  25692  itg2splitlem  25722  itg2monolem1  25724  itg2cnlem1  25735  dvne0  25989  lhop1lem  25991  deg1nn0clb  26068  dgrle  26221  coemulhi  26232  aaliou3lem9  26331  cos11  26515  logleb  26585  argrege0  26593  logdivle  26604  ellogdm  26621  cxple  26677  cxplt2  26680  cxple3  26683  isosctrlem1  26801  atandm  26859  atans2  26914  atantayl2  26921  eldmgm  27005  ftalem7  27062  isppw2  27098  musum  27174  dchrsum2  27252  bposlem1  27268  lgsmod  27307  lgsdir2lem2  27310  lgsdir2  27314  lgsne0  27319  lgsprme0  27323  gausslemma2dlem4  27353  lgsquadlem1  27364  2lgslem3  27388  2lgsoddprm  27400  2sq2  27417  addsqrexnreu  27426  rpvmasumlem  27471  padicabv  27614  ostth3  27622  ostth  27623  noextenddif  27653  nodenselem4  27672  nodenselem5  27673  nodenselem7  27675  nolt02o  27680  nogt01o  27681  noresle  27682  nosupprefixmo  27685  noinfprefixmo  27686  nosupcbv  27687  nosupdm  27689  nosupfv  27691  nosupres  27692  nosupbnd1lem1  27693  nosupbnd1lem3  27695  nosupbnd1lem5  27697  nosupbnd1  27699  nosupbnd2lem1  27700  nosupbnd2  27701  noinfcbv  27702  noinfdm  27704  noinffv  27706  noinfres  27707  noinfbnd1lem1  27708  noinfbnd1lem3  27710  noinfbnd1lem5  27712  noinfbnd1  27714  noinfbnd2lem1  27715  noinfbnd2  27716  lenlts  27737  ltsne  27759  nocvxminlem  27767  lesrec  27812  eqcuts3  27817  cuteq1  27830  newbday  27915  ltslpss  27921  cofcutr  27937  lrrecfr  27956  addsval  27975  ltadds2  28004  lenegs  28059  lesubsubsbd  28099  lesubsubs2bd  28100  lesubsubs3bd  28101  lesubaddsd  28106  ltmuls2  28184  lemuls2d  28187  lemuls1d  28188  oncutlt  28277  onles  28281  pw2cut2  28475  bdaypw2bnd  28478  bdayfinbndlem1  28480  istrkgld  28548  axtgupdim2  28561  tglowdim2l  28740  axlowdimlem16  29048  axlowdim2  29051  axlowdim  29052  numedglnl  29235  usgredg2v  29318  lfuhgr1v0e  29345  cusgrfi  29550  vtxd0nedgb  29580  vtxduhgr0edgnel  29586  1loopgrnb0  29594  1hevtxdg0  29597  vtxdgoddnumeven  29645  wlkp1lem1  29763  wlkp1lem2  29764  wlkp1lem5  29767  dfpth2  29820  crctcsh  29915  clwlkclwwlklem2a4  30090  eupth2eucrct  30310  eupth2lem3lem3  30323  eupth2lem3lem4  30324  eupth2lem3lem6  30326  eupth2lem3lem7  30327  eupth2lems  30331  eupth2  30332  konigsberglem4  30348  nfrgr2v  30365  frgrwopreglem3  30407  fusgr2wsp2nb  30427  frgrreggt1  30486  friendshipgt3  30491  lpni  30574  nmobndseqi  30873  minvecolem5  30975  chpsscon3  31597  chnle  31608  nonbooli  31745  pjnel  31820  specval  31992  nmcfnlbi  32146  stri  32351  hstri  32359  cvbr  32376  cvcon3  32378  chcv1  32449  cvexchlem  32462  chrelat2  32464  nelun  32606  elpreq  32621  nelpr  32624  ifeqeqx  32635  nfpconfp  32728  suppiniseg  32782  isoun  32798  suppss3  32819  xrge0infss  32857  infxrge0gelb  32863  eliccelico  32874  elicoelioo  32875  nndiffz1  32883  hashgt1  32905  expgt0b  32914  nn0min  32918  ccatws1f1o  33050  toslublem  33071  tosglblem  33073  pmtrcnel  33189  cycpmco2  33233  isarchi2  33285  archiabl  33298  elrgspnlem2  33343  elrgspnlem3  33344  0nellinds  33469  lindssn  33477  lindfpropd  33481  ssdifidlprm  33557  mxidlirred  33571  ssmxidl  33573  esplyind  33758  lbslsat  33800  lindsunlem  33808  rtelextdg2lem  33910  constrsqrtcl  33963  ordtcnvNEW  34104  ordtrestNEW  34105  ordtrest2NEWlem  34106  ordtrest2NEW  34107  ordtconnlem1  34108  xrge0iifcnv  34117  esumpcvgval  34262  esum2d  34277  ddemeas  34420  omssubadd  34484  oddpwdc  34538  eulerpartlems  34544  eulerpartlemf  34554  eulerpartlemt  34555  eulerpartlemr  34558  eulerpartlemgvv  34560  eulerpartlemn  34565  ballotlemfc0  34677  ballotlemfcc  34678  ballotlem4  34683  ballotlemimin  34690  ballotlem7  34720  plymulx  34732  signsply0  34735  reprinfz1  34806  reprpmtf1o  34810  reprdifc  34811  hgt750lema  34841  hgt750leme  34842  istrkg2d  34850  bnj23  34901  bnj1185  34975  bnj1228  35193  bnj1388  35215  bnj1417  35223  nummin  35276  axnulg  35291  axprALT2  35293  fineqvnttrclselem1  35305  onvf1odlem2  35326  onvf1odlem3  35327  revwlk  35347  isacycgr  35367  acycgr0v  35370  prclisacycgr  35373  erdszelem10  35422  satf0n0  35600  fmlaomn0  35612  fmlasucdisj  35621  satfv1fvfmla1  35645  satefvfmla1  35647  ismfs  35771  mvtinf  35777  untelirr  35930  untsucf  35932  untangtr  35936  dfon2lem3  36005  dfon2lem4  36006  dfon2lem7  36009  dfon2lem9  36011  distel  36023  funpartfv  36167  dfrdg4  36173  nn0prpwlem  36544  nn0prpw  36545  limsucncmpi  36667  limsucncmp  36668  ordcmp  36669  weiunlem  36685  weiunfrlem  36686  weiunfr  36689  regsfromregtr  36696  regsfromsetind  36697  unblimceq0  36735  unbdqndv1  36736  bj-hbntbi  36969  bj-equsexvwd  37038  bj-cbvexdv  37075  bj-ru1  37218  bj-nuliota  37332  topdifinffinlem  37629  topdifinffin  37630  icorempo  37633  relowlpssretop  37646  finxpreclem2  37672  finxpreclem6  37678  wl-issetft  37866  wl-eujustlem1  37872  leceifl  37889  lindsadd  37893  lindsenlbs  37895  matunitlindflem1  37896  poimirlem16  37916  poimirlem17  37917  poimirlem18  37918  poimirlem19  37919  poimirlem21  37921  poimirlem23  37923  poimirlem26  37926  poimirlem27  37927  poimirlem28  37928  poimirlem31  37931  poimir  37933  mblfinlem2  37938  mblfinlem3  37939  ismblfin  37941  cnambfre  37948  itg2addnclem  37951  itg2addnclem2  37952  iblabsnclem  37963  ftc1anclem1  37973  areacirc  37993  heibor1lem  38089  heiborlem1  38091  heiborlem6  38096  heiborlem8  38098  heiborlem10  38100  smprngopr  38332  ecin0  38632  ax12inda  39353  riotaclbgBAD  39359  lcvfbr  39425  lcvbr  39426  lsatcv0  39436  l1cvpat  39459  opltcon3b  39609  cvrfval  39673  cvrval  39674  cvrnbtwn  39676  cvrval2  39679  cvrnbtwn2  39680  cvrnbtwn3  39681  cvrcon3b  39682  cvrnbtwn4  39684  atnlt  39718  iscvlat  39728  cvlexch1  39733  hlsuprexch  39786  hlrelat5N  39806  hlrelat2  39808  cvrval5  39820  3dimlem1  39863  3dim1lem5  39871  3dim2  39873  3dim3  39874  llnnlt  39928  islpln5  39940  lplni2  39942  lvolex3N  39943  lplnnle2at  39946  islpln2a  39953  lplnribN  39956  lplnexllnN  39969  lplnnlt  39970  lvoli3  39982  islvol5  39984  lvoli2  39986  lvolnle3at  39987  islvol2aN  39997  4atlem11  40014  lvolnltN  40023  dalawlem15  40290  4atexlemex2  40476  4atex  40481  4atex2-0aOLDN  40483  4atex2-0cOLDN  40485  lautcvr  40497  ltrnfset  40522  ltrnset  40523  ltrnu  40526  trlfset  40565  trlset  40566  trlval2  40568  cdlemd6  40608  cdleme0nex  40695  cdleme18d  40700  cdleme25b  40759  cdleme25cv  40763  cdleme29b  40780  cdleme31fv  40795  cdleme31fv2  40798  cdlemefrs29bpre0  40801  cdlemefr32sn2aw  40809  cdlemefr29bpre0N  40811  cdlemefr29clN  40812  cdlemefr32fvaN  40814  cdlemefr32fva1  40815  cdlemefs32sn1aw  40819  cdleme32fva  40842  cdleme32fvaw  40844  cdleme40v  40874  cdleme42b  40883  cdleme46f2g2  40898  cdleme46f2g1  40899  cdleme48gfv  40942  cdlemg1fvawlemN  40978  cdlemg1cex  40993  cdlemg6d  41026  cdlemm10N  41523  dicffval  41579  dicfval  41580  dicval  41581  dicfnN  41588  dicvalrelN  41590  dihffval  41635  dihfval  41636  dihlsscpre  41639  dvh4dimat  41843  dvh3dimatN  41844  dvh4dimlem  41848  dvh3dim  41851  dvh4dimN  41852  dvh3dim2  41853  dvh3dim3N  41854  mapdcv  42065  mapdh9aOLDN  42195  hdmapfval  42232  hdmapval  42233  hdmapval2  42237  hdmap11lem2  42247  dvrelog2b  42465  aks4d1p4  42478  aks4d1p5  42479  aks4d1p7  42482  aks4d1p8d2  42484  aks4d1p8  42486  aks4d1  42488  aks6d1c2p2  42518  hashnexinj  42527  rspcsbnea  42530  aks6d1c5  42538  aks6d1c6lem3  42571  aks6d1c7  42583  supinf  42641  oexpreposd  42721  mullt0b2d  42883  flt4lem7  43046  nna4b4nsq  43047  ellz1  43153  rencldnfilem  43206  jm2.22  43381  jm2.23  43382  wepwsolem  43428  fnwe2lem2  43437  aomclem8  43447  unxpwdom3  43481  onsupmaxb  43625  onexlimgt  43629  onsupeqnmax  43633  onov0suclim  43660  oaordnr  43682  omnord1  43691  oenord1  43702  oaomoencom  43703  oenass  43705  cantnfresb  43710  tfsnfin  43738  ralopabb  43796  nlimsuc  43826  ifpbi12  43873  dfsucon  43908  sqrtcvallem1  44016  ss2iundf  44044  frege124d  44146  clsk3nimkb  44425  clsk1indlem1  44430  clsk1independent  44431  ntrneineine1lem  44469  ntrneicls11  44475  clsneiel1  44493  clsneiel2  44494  neicvgel1  44504  neicvgel2  44505  radcnvrat  44699  rusbcALT  44823  en3lpVD  45229  0elaxnul  45368  omssaxinf2  45373  permaxnul  45393  permaxinf2lem  45397  nregmodel  45402  eliin2f  45492  nssd  45493  wessf1ornlem  45573  rexanuz2nf  45879  limsupre2lem  46111  icccncfext  46274  stoweidlem14  46401  stoweidlem34  46421  stoweidlem59  46446  etransclem24  46645  nnfoctbdjlem  46842  nnfoctbdj  46843  hspmbllem2  47014  nsssmfmbflem  47165  fsetsnprcnex  47444  eu2ndop1stv  47514  afvfv0bi  47541  afvco2  47565  ndmaovg  47573  ndfatafv2nrn  47610  afv2ndefb  47613  afv2fv0  47654  nelbr  47663  otiunsndisjX  47668  fun2dmnopgexmpl  47673  ltnltne  47688  readdcnnred  47692  resubcnnred  47693  recnmulnred  47694  cndivrenred  47695  ichnreuop  47861  fmtnoinf  47925  odz2prm2pw  47952  prmdvdsfmtnof1lem2  47974  lighneallem3  47996  lighneallem4  47999  requad1  48011  isodd3  48041  bits0ALTV  48068  nfermltl8rev  48131  nfermltl2rev  48132  nfermltlrev  48133  upgrimpths  48298  isubgr3stgrlem3  48357  usgrexmpl12ngric  48427  pgnbgreunbgrlem2lem1  48503  pgnbgreunbgrlem2lem2  48504  pgnbgreunbgrlem2lem3  48505  pgnbgreunbgrlem5lem1  48509  pgnbgreunbgrlem5lem2  48510  pgnbgreunbgrlem5lem3  48511  lgricngricex  48518  lidldomnnring  48625  ztprmneprm  48736  lindepsnlininds  48841  islindeps  48842  lindslinindsimp2lem5  48851  lindslinindsimp2  48852  line2ylem  49140  line2xlem  49142  map0cor  49243  nelsubc3lem  49458  fulltermc2  49900  setc1onsubc  49990  cnelsubclem  49991  elsetrecslem  50087