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  2345  cbvex2v  2347  drex1v  2373  cbvex  2402  cbvex2  2415  drex1  2444  eujustALT  2571  necon3abid  2966  neleq12d  3039  cbvrexdva  3216  cbvrexfw  3276  cbvrexdva2  3312  cbvrexf  3321  cbvexeqsetf  3442  ceqsex  3475  ceqsexv  3476  gencbval  3487  spcegf  3532  spc2gv  3540  spc2d  3542  spc3gv  3544  ceqsralbv  3597  cdeqnot  3711  rru  3722  ruOLD  3724  sbcng  3772  sbcrext  3807  cbvrexcsf  3876  difjust  3887  eldif  3895  dfpss3  4022  dfdif3OLD  4051  difeq2  4053  disjne  4385  pssdifcom1  4419  eldifpr  4592  rexsng  4610  elpwunsn  4618  eldiftp  4621  rexprg  4631  preqsnd  4792  disjxun  5072  exnelv  5237  nalsetOLD  5239  dtruALT2  5301  dtruALT  5319  rexxfrd  5340  rexxfr2d  5342  rexxfrd2  5344  rexxfr  5347  opthneg  5423  snopeqop  5449  otiunsndisj  5463  poeq1  5531  pocl  5536  swopo  5539  sotric  5558  sotrieq  5559  isso2i  5565  somo  5567  freq1  5587  frirr  5596  fr2nr  5597  frminex  5599  tz7.2  5603  wereu2  5617  poinxp  5701  frinxp  5703  posn  5706  frsn  5708  rexiunxp  5784  rexxpf  5791  intirr  6070  poirr2  6076  cnvpo  6240  dfpo2  6249  predpoirr  6286  predfrirr  6287  frpomin  6293  nordeq  6331  ordtri1  6345  ordtri3  6348  fvmpti  6935  fndmdif  6983  rexrnmptw  7036  rexrnmpt  7038  rexima  7182  f1imapss  7210  f1ounsn  7216  cbvexfo  7234  nf1const  7248  soisoi  7272  isopolem  7289  weniso  7298  imaeqsalvOLD  7308  canth  7310  riotaclb  7354  rexrnmpo  7496  ndmovg  7539  sorpssuni  7675  sorpssint  7676  fr3nr  7715  dfwe2  7717  ordsucsssuc  7763  nlimsucg  7782  orduninsuc  7783  dfom2  7808  ssnlim  7826  resf1extb  7874  f1oweALT  7914  frxp  8065  poxp  8067  frxp2  8083  frxp3  8090  xpord3inddlem  8093  soseq  8098  suppofssd  8142  suppcoss  8146  smoword  8295  tz7.48lem  8369  oacan  8472  oaword  8473  omlimcl  8502  omeulem1  8506  nnaword  8552  nnmword  8558  nneob  8581  naddss1  8614  brdifun  8663  swoer  8664  undifixp  8871  boxcutc  8878  2dom  8966  php  9130  phpeqd  9135  nndomog  9136  onomeneq  9137  nnsdomo  9142  unxpdomlem2  9156  frfi  9184  unfilem1  9204  tfsnfin2  9262  supeq3  9351  supeq123d  9352  supmo  9354  eqsup  9358  supub  9361  sup0  9369  suppr  9374  supisolem  9376  supisoex  9377  eqinf  9387  infval  9389  infmo  9399  infpr  9407  infempty  9411  oieq1  9416  ordtypecbv  9421  ordtypelem7  9428  wemapsolem  9454  canthwdom  9483  zfregcl  9498  zfregclOLD  9499  elirrv  9501  elirrvOLD  9502  elirr  9503  noinfep  9570  cantnfp1lem3  9590  ttrcltr  9626  rankr1clem  9733  carden2b  9880  domtri2  9902  alephord3  9989  alephdom2  9998  alephval3  10021  dfac9  10048  kmlem2  10063  kmlem4  10065  isfin4  10208  isfin7  10212  fin23lem11  10228  isf32lem5  10268  isf34lem4  10288  fin1a2lem6  10316  fin1a2lem7  10317  fin1a2lem12  10322  itunisuc  10330  ac6n  10396  zorn2g  10414  zornn0g  10416  ttukeylem7  10426  infinfg  10477  axpowndlem3  10511  axpowndlem4  10512  axregnd  10516  elgch  10534  engch  10540  fpwwe2lem12  10554  fpwwe2  10555  pwfseqlem1  10570  pwfseqlem3  10572  hargch  10585  addnidpi  10813  pinq  10839  nqereu  10841  ltsonq  10881  prlem934  10945  ltexprlem7  10954  addcanpr  10958  prlem936  10959  reclem2pr  10960  reclem3pr  10961  supexpr  10966  ltsosr  11006  supsrlem  11023  axpre-lttri  11077  axpre-sup  11081  xrlenlt  11199  axlttri  11206  axsup  11210  ltne  11232  dedekind  11298  readdcan  11309  leadd1  11607  ltsub1  11635  ltsub2  11636  leord1  11666  lediv1  12010  lemuldiv  12025  lerec  12028  le2msq  12045  infm3  12104  suprnub  12110  infregelb  12129  avgle1  12406  avgle2  12407  znnnlt1  12543  indstr  12855  zsupss  12876  uzsupss  12879  rpneg  12965  xralrple  13146  xleneg  13159  xltadd1  13197  xposdif  13203  xmulneg1  13210  xltmul1  13233  xrsupexmnf  13246  xrinfmexpnf  13247  xrsupsslem  13248  xrinfmsslem  13249  xrub  13253  supxrleub  13267  infxrgelb  13277  difreicc  13426  nn0disj  13587  nelfzo  13608  elfznelfzo  13717  fvinim0ffz  13733  injresinjlem  13734  ssnn0fi  13936  leexp2  14122  exp11nnd  14212  hashbnd  14287  hasheni  14299  hashfundm  14393  hashbc  14404  wrdsymb0  14500  swrdnd  14606  swrdnd2  14607  pfxnd0  14640  repswswrd  14735  repswccat  14737  cshwidxmod  14754  cnpart  15191  sqrtlt  15212  limsuplt  15430  rlimrege0  15530  isercoll  15619  efle  16074  odd2np1  16299  sumodd  16346  divalglem7  16357  ndvdsadd  16368  fldivndvdslt  16374  bitsfval  16381  bitsval  16382  bits0  16386  bitsp1  16389  bitsmod  16394  bitscmp  16396  bitsinv1lem  16399  sadadd2lem2  16408  saddisjlem  16422  bitsshft  16433  gcdneg  16480  algcvgblem  16535  lcmneg  16561  isprm3  16641  dvdsnprmd  16648  isprm5  16666  rpexp  16681  phiprmpw  16735  m1dvdsndvds  16758  pythagtrip  16794  pcgcd1  16837  prmpwdvds  16864  prmreclem2  16877  prmreclem3  16878  prmreclem5  16880  prmreclem6  16881  vdwlem6  16946  vdwnnlem2  16956  vdwnnlem3  16957  vdwnn  16958  prmlem0  17065  prmlem1a  17066  divsfval  17500  mrisval  17585  ismri  17586  ismri2dad  17592  cidpropd  17665  cat1lem  18052  plttr  18295  joinval  18330  meetval  18344  acsfiindd  18508  isnsgrp  18680  smndex1n0mnd  18872  mgm2nsgrplem2  18879  sgrp2nmndlem3  18885  symgpssefmnd  19360  symgfix2  19380  pmtrdifellem4  19443  psgnunilem1  19457  psgnunilem5  19458  psgnunilem2  19459  psgnunilem3  19460  pmtrsn  19483  sylow1lem3  19564  sylow2alem2  19582  efgsfo  19703  ablfac1eulem  20038  ablfac1eu  20039  pgpfac1lem1  20040  pgpfac1lem5  20045  nzrunit  20490  zrninitoringc  20642  islbs  21060  lbsind  21064  lbspss  21066  lbspropd  21083  lspsnne1  21104  islbs2  21141  lbsacsbs  21143  lbsextlem1  21145  lbsextlem3  21147  lbsextlem4  21148  lbsextg  21149  frlmlbs  21766  islindf  21781  islinds2  21782  islindf2  21783  lindfind  21785  lindsind  21786  lindfrn  21790  lindfmm  21796  lsslindf  21799  islindf4  21807  opsrtoslem2  22023  psdmul  22121  cply1coe0  22254  cply1coe0bi  22255  mdetunilem7  22571  mdetunilem8  22572  mdetunilem9  22573  maducoeval2  22593  pmatcollpw3fi1lem1  22739  fvmptnn04ifa  22803  fvmptnn04ifc  22805  fvmptnn04ifd  22806  chfacffsupp  22809  chfacfscmul0  22811  chfacfpmmul0  22815  elcls  23026  maxlp  23100  perfi  23108  ordtbaslem  23141  ordtval  23142  ordtbas2  23144  ordtopn1  23147  ordtopn2  23148  ordtcnv  23154  ordtrest  23155  ordtrest2lem  23156  ordtrest2  23157  pnfnei  23173  mnfnei  23174  isreg2  23330  ordthauslem  23336  cmpfi  23361  cmpfii  23362  bwth  23363  nconnsubb  23376  hausdiag  23598  txkgen  23605  kqdisj  23685  ordthmeolem  23754  fbfinnfr  23794  trfbas  23797  fbunfip  23822  fbasrn  23837  trfil3  23841  ufileu  23872  fin1aufil  23885  hausflim  23934  alexsubALTlem2  24001  alexsubALTlem3  24002  alexsubALTlem4  24003  ptcmplem2  24006  ptcmplem3  24007  stdbdbl  24470  iccntr  24775  reconnlem2  24781  iccpnfcnv  24899  xrhmeo  24901  lebnumlem1  24916  lebnumlem2  24917  lebnumlem3  24918  bcthlem4  25282  minveclem3b  25383  ivthlem2  25407  ivthlem3  25408  mbfmax  25604  mbfposr  25607  i1fd  25636  mbfi1fseqlem4  25673  itg2splitlem  25703  itg2monolem1  25705  itg2cnlem1  25716  dvne0  25966  lhop1lem  25968  deg1nn0clb  26043  dgrle  26196  coemulhi  26207  aaliou3lem9  26304  cos11  26485  logleb  26555  argrege0  26563  logdivle  26574  ellogdm  26591  cxple  26647  cxplt2  26650  cxple3  26653  isosctrlem1  26770  atandm  26828  atans2  26883  atantayl2  26890  eldmgm  26973  ftalem7  27030  isppw2  27066  musum  27142  dchrsum2  27219  bposlem1  27235  lgsmod  27274  lgsdir2lem2  27277  lgsdir2  27281  lgsne0  27286  lgsprme0  27290  gausslemma2dlem4  27320  lgsquadlem1  27331  2lgslem3  27355  2lgsoddprm  27367  2sq2  27384  addsqrexnreu  27393  rpvmasumlem  27438  padicabv  27581  ostth3  27589  ostth  27590  noextenddif  27620  nodenselem4  27639  nodenselem5  27640  nodenselem7  27642  nolt02o  27647  nogt01o  27648  noresle  27649  nosupprefixmo  27652  noinfprefixmo  27653  nosupcbv  27654  nosupdm  27656  nosupfv  27658  nosupres  27659  nosupbnd1lem1  27660  nosupbnd1lem3  27662  nosupbnd1lem5  27664  nosupbnd1  27666  nosupbnd2lem1  27667  nosupbnd2  27668  noinfcbv  27669  noinfdm  27671  noinffv  27673  noinfres  27674  noinfbnd1lem1  27675  noinfbnd1lem3  27677  noinfbnd1lem5  27679  noinfbnd1  27681  noinfbnd2lem1  27682  noinfbnd2  27683  lenlts  27704  ltsne  27726  nocvxminlem  27734  lesrec  27779  eqcuts3  27784  cuteq1  27797  newbday  27882  ltslpss  27888  cofcutr  27904  lrrecfr  27923  addsval  27942  ltadds2  27971  lenegs  28026  lesubsubsbd  28066  lesubsubs2bd  28067  lesubsubs3bd  28068  lesubaddsd  28073  ltmuls2  28151  lemuls2d  28154  lemuls1d  28155  oncutlt  28244  onles  28248  pw2cut2  28442  bdaypw2bnd  28445  bdayfinbndlem1  28447  istrkgld  28515  axtgupdim2  28527  tglowdim2l  28706  axlowdimlem16  29014  axlowdim2  29017  axlowdim  29018  numedglnl  29201  usgredg2v  29284  lfuhgr1v0e  29311  cusgrfi  29515  vtxd0nedgb  29545  vtxduhgr0edgnel  29551  1loopgrnb0  29559  1hevtxdg0  29562  vtxdgoddnumeven  29610  wlkp1lem1  29728  wlkp1lem2  29729  wlkp1lem5  29732  dfpth2  29785  crctcsh  29880  clwlkclwwlklem2a4  30055  eupth2eucrct  30275  eupth2lem3lem3  30288  eupth2lem3lem4  30289  eupth2lem3lem6  30291  eupth2lem3lem7  30292  eupth2lems  30296  eupth2  30297  konigsberglem4  30313  nfrgr2v  30330  frgrwopreglem3  30372  fusgr2wsp2nb  30392  frgrreggt1  30451  friendshipgt3  30456  lpni  30539  nmobndseqi  30838  minvecolem5  30940  chpsscon3  31562  chnle  31573  nonbooli  31710  pjnel  31785  specval  31957  nmcfnlbi  32111  stri  32316  hstri  32324  cvbr  32341  cvcon3  32343  chcv1  32414  cvexchlem  32427  chrelat2  32429  nelun  32571  elpreq  32586  nelpr  32589  ifeqeqx  32600  nfpconfp  32693  suppiniseg  32747  isoun  32763  suppss3  32784  xrge0infss  32821  infxrge0gelb  32827  eliccelico  32838  elicoelioo  32839  nndiffz1  32847  hashgt1  32869  expgt0b  32878  nn0min  32882  ccatws1f1o  32999  toslublem  33020  tosglblem  33022  pmtrcnel  33138  cycpmco2  33182  isarchi2  33234  archiabl  33247  elrgspnlem2  33292  elrgspnlem3  33293  0nellinds  33418  lindssn  33426  lindfpropd  33430  ssdifidlprm  33506  mxidlirred  33520  ssmxidl  33522  esplyind  33707  lbslsat  33748  lindsunlem  33756  rtelextdg2lem  33858  constrsqrtcl  33911  ordtcnvNEW  34052  ordtrestNEW  34053  ordtrest2NEWlem  34054  ordtrest2NEW  34055  ordtconnlem1  34056  xrge0iifcnv  34065  esumpcvgval  34210  esum2d  34225  ddemeas  34368  omssubadd  34432  oddpwdc  34486  eulerpartlems  34492  eulerpartlemf  34502  eulerpartlemt  34503  eulerpartlemr  34506  eulerpartlemgvv  34508  eulerpartlemn  34513  ballotlemfc0  34625  ballotlemfcc  34626  ballotlem4  34631  ballotlemimin  34638  ballotlem7  34668  plymulx  34680  signsply0  34683  reprinfz1  34754  reprpmtf1o  34758  reprdifc  34759  hgt750lema  34789  hgt750leme  34790  istrkg2d  34798  bnj23  34849  bnj1185  34923  bnj1228  35141  bnj1388  35163  bnj1417  35171  nummin  35224  axnulg  35239  axprALT2  35241  fineqvnttrclselem1  35253  onvf1odlem2  35274  onvf1odlem3  35275  revwlk  35295  isacycgr  35315  acycgr0v  35318  prclisacycgr  35321  erdszelem10  35370  satf0n0  35548  fmlaomn0  35560  fmlasucdisj  35569  satfv1fvfmla1  35593  satefvfmla1  35595  ismfs  35719  mvtinf  35725  untelirr  35878  untsucf  35880  untangtr  35884  dfon2lem3  35953  dfon2lem4  35954  dfon2lem7  35957  dfon2lem9  35959  distel  35971  funpartfv  36115  dfrdg4  36121  nn0prpwlem  36492  nn0prpw  36493  limsucncmpi  36615  limsucncmp  36616  ordcmp  36617  weiunlem  36633  weiunfrlem  36634  weiunfr  36637  axtcond  36648  regsfromregtco  36708  regsfromsetind  36709  unblimceq0  36755  unbdqndv1  36756  bj-hbntbi  36989  bj-equsexvwd  37058  bj-cbvexdv  37095  bj-ru1  37238  bj-nuliota  37352  topdifinffinlem  37651  topdifinffin  37652  icorempo  37655  relowlpssretop  37668  finxpreclem2  37694  finxpreclem6  37700  wl-issetft  37895  wl-eujustlem1  37901  leceifl  37918  lindsadd  37922  lindsenlbs  37924  matunitlindflem1  37925  poimirlem16  37945  poimirlem17  37946  poimirlem18  37947  poimirlem19  37948  poimirlem21  37950  poimirlem23  37952  poimirlem26  37955  poimirlem27  37956  poimirlem28  37957  poimirlem31  37960  poimir  37962  mblfinlem2  37967  mblfinlem3  37968  ismblfin  37970  cnambfre  37977  itg2addnclem  37980  itg2addnclem2  37981  iblabsnclem  37992  ftc1anclem1  38002  areacirc  38022  heibor1lem  38118  heiborlem1  38120  heiborlem6  38125  heiborlem8  38127  heiborlem10  38129  smprngopr  38361  ecin0  38661  ax12inda  39382  riotaclbgBAD  39388  lcvfbr  39454  lcvbr  39455  lsatcv0  39465  l1cvpat  39488  opltcon3b  39638  cvrfval  39702  cvrval  39703  cvrnbtwn  39705  cvrval2  39708  cvrnbtwn2  39709  cvrnbtwn3  39710  cvrcon3b  39711  cvrnbtwn4  39713  atnlt  39747  iscvlat  39757  cvlexch1  39762  hlsuprexch  39815  hlrelat5N  39835  hlrelat2  39837  cvrval5  39849  3dimlem1  39892  3dim1lem5  39900  3dim2  39902  3dim3  39903  llnnlt  39957  islpln5  39969  lplni2  39971  lvolex3N  39972  lplnnle2at  39975  islpln2a  39982  lplnribN  39985  lplnexllnN  39998  lplnnlt  39999  lvoli3  40011  islvol5  40013  lvoli2  40015  lvolnle3at  40016  islvol2aN  40026  4atlem11  40043  lvolnltN  40052  dalawlem15  40319  4atexlemex2  40505  4atex  40510  4atex2-0aOLDN  40512  4atex2-0cOLDN  40514  lautcvr  40526  ltrnfset  40551  ltrnset  40552  ltrnu  40555  trlfset  40594  trlset  40595  trlval2  40597  cdlemd6  40637  cdleme0nex  40724  cdleme18d  40729  cdleme25b  40788  cdleme25cv  40792  cdleme29b  40809  cdleme31fv  40824  cdleme31fv2  40827  cdlemefrs29bpre0  40830  cdlemefr32sn2aw  40838  cdlemefr29bpre0N  40840  cdlemefr29clN  40841  cdlemefr32fvaN  40843  cdlemefr32fva1  40844  cdlemefs32sn1aw  40848  cdleme32fva  40871  cdleme32fvaw  40873  cdleme40v  40903  cdleme42b  40912  cdleme46f2g2  40927  cdleme46f2g1  40928  cdleme48gfv  40971  cdlemg1fvawlemN  41007  cdlemg1cex  41022  cdlemg6d  41055  cdlemm10N  41552  dicffval  41608  dicfval  41609  dicval  41610  dicfnN  41617  dicvalrelN  41619  dihffval  41664  dihfval  41665  dihlsscpre  41668  dvh4dimat  41872  dvh3dimatN  41873  dvh4dimlem  41877  dvh3dim  41880  dvh4dimN  41881  dvh3dim2  41882  dvh3dim3N  41883  mapdcv  42094  mapdh9aOLDN  42224  hdmapfval  42261  hdmapval  42262  hdmapval2  42266  hdmap11lem2  42276  dvrelog2b  42493  aks4d1p4  42506  aks4d1p5  42507  aks4d1p7  42510  aks4d1p8d2  42512  aks4d1p8  42514  aks4d1  42516  aks6d1c2p2  42546  hashnexinj  42555  rspcsbnea  42558  aks6d1c5  42566  aks6d1c6lem3  42599  aks6d1c7  42611  supinf  42669  oexpreposd  42742  mullt0b2d  42917  flt4lem7  43080  nna4b4nsq  43081  ellz1  43187  rencldnfilem  43236  jm2.22  43411  jm2.23  43412  wepwsolem  43458  fnwe2lem2  43467  aomclem8  43477  unxpwdom3  43511  onsupmaxb  43655  onexlimgt  43659  onsupeqnmax  43663  onov0suclim  43690  oaordnr  43712  omnord1  43721  oenord1  43732  oaomoencom  43733  oenass  43735  cantnfresb  43740  tfsnfin  43768  ralopabb  43826  nlimsuc  43856  ifpbi12  43903  dfsucon  43938  sqrtcvallem1  44046  ss2iundf  44074  frege124d  44176  clsk3nimkb  44455  clsk1indlem1  44460  clsk1independent  44461  ntrneineine1lem  44499  ntrneicls11  44505  clsneiel1  44523  clsneiel2  44524  neicvgel1  44534  neicvgel2  44535  radcnvrat  44729  rusbcALT  44853  en3lpVD  45259  0elaxnul  45398  omssaxinf2  45403  permaxnul  45423  permaxinf2lem  45427  nregmodel  45432  eliin2f  45522  nssd  45523  wessf1ornlem  45603  rexanuz2nf  45908  limsupre2lem  46140  icccncfext  46303  stoweidlem14  46430  stoweidlem34  46450  stoweidlem59  46475  etransclem24  46674  nnfoctbdjlem  46871  nnfoctbdj  46872  hspmbllem2  47043  nsssmfmbflem  47194  fsetsnprcnex  47491  eu2ndop1stv  47561  afvfv0bi  47588  afvco2  47612  ndmaovg  47620  ndfatafv2nrn  47657  afv2ndefb  47660  afv2fv0  47701  nelbr  47710  otiunsndisjX  47715  fun2dmnopgexmpl  47720  ltnltne  47735  readdcnnred  47739  resubcnnred  47740  recnmulnred  47741  cndivrenred  47742  ichnreuop  47920  nprmmul1  47975  fmtnoinf  47987  odz2prm2pw  48014  prmdvdsfmtnof1lem2  48036  lighneallem3  48058  lighneallem4  48061  requad1  48086  isodd3  48116  bits0ALTV  48143  nfermltl8rev  48206  nfermltl2rev  48207  nfermltlrev  48208  upgrimpths  48373  isubgr3stgrlem3  48432  usgrexmpl12ngric  48502  pgnbgreunbgrlem2lem1  48578  pgnbgreunbgrlem2lem2  48579  pgnbgreunbgrlem2lem3  48580  pgnbgreunbgrlem5lem1  48584  pgnbgreunbgrlem5lem2  48585  pgnbgreunbgrlem5lem3  48586  lgricngricex  48593  lidldomnnring  48700  ztprmneprm  48811  lindepsnlininds  48916  islindeps  48917  lindslinindsimp2lem5  48926  lindslinindsimp2  48927  line2ylem  49215  line2xlem  49217  map0cor  49318  nelsubc3lem  49533  fulltermc2  49975  setc1onsubc  50065  cnelsubclem  50066  elsetrecslem  50162