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  cbvrexdva2  3315  cbvrexf  3324  cbvexeqsetf  3445  ceqsex  3478  ceqsexv  3479  gencbval  3490  spcegf  3535  spc2gv  3543  spc2d  3545  spc3gv  3547  ceqsralbv  3600  cdeqnot  3715  rru  3726  ruOLD  3728  sbcng  3777  sbcrext  3812  cbvrexcsf  3881  difjust  3892  eldif  3900  dfpss3  4030  dfdif3OLD  4059  difeq2  4061  disjne  4396  pssdifcom1  4430  eldifpr  4603  rexsng  4621  elpwunsn  4629  eldiftp  4632  rexprg  4642  preqsnd  4803  disjxun  5084  exnelv  5249  nalsetOLD  5251  dtruALT2  5311  dtruALT  5329  rexxfrd  5350  rexxfr2d  5352  rexxfrd2  5354  rexxfr  5357  opthneg  5433  snopeqop  5458  otiunsndisj  5472  poeq1  5539  pocl  5544  swopo  5547  sotric  5566  sotrieq  5567  isso2i  5573  somo  5575  freq1  5595  frirr  5604  fr2nr  5605  frminex  5607  tz7.2  5611  wereu2  5625  poinxp  5709  frinxp  5711  posn  5714  frsn  5716  rexiunxp  5793  rexxpf  5800  intirr  6079  poirr2  6085  cnvpo  6249  dfpo2  6258  predpoirr  6295  predfrirr  6296  frpomin  6302  nordeq  6340  ordtri1  6354  ordtri3  6357  fvmpti  6944  fndmdif  6992  rexrnmptw  7045  rexrnmpt  7047  rexima  7190  f1imapss  7218  f1ounsn  7224  cbvexfo  7242  nf1const  7256  soisoi  7280  isopolem  7297  weniso  7306  imaeqsalvOLD  7316  canth  7318  riotaclb  7362  rexrnmpo  7504  ndmovg  7547  sorpssuni  7683  sorpssint  7684  fr3nr  7723  dfwe2  7725  ordsucsssuc  7771  nlimsucg  7790  orduninsuc  7791  dfom2  7816  ssnlim  7834  resf1extb  7882  f1oweALT  7922  frxp  8073  poxp  8075  frxp2  8091  frxp3  8098  xpord3inddlem  8101  soseq  8106  suppofssd  8150  suppcoss  8154  smoword  8303  tz7.48lem  8377  oacan  8480  oaword  8481  omlimcl  8510  omeulem1  8514  nnaword  8560  nnmword  8566  nneob  8589  naddss1  8622  brdifun  8671  swoer  8672  undifixp  8879  boxcutc  8886  2dom  8974  php  9138  phpeqd  9143  nndomog  9144  onomeneq  9145  nnsdomo  9150  unxpdomlem2  9164  frfi  9192  unfilem1  9212  tfsnfin2  9270  supeq3  9359  supeq123d  9360  supmo  9362  eqsup  9366  supub  9369  sup0  9377  suppr  9382  supisolem  9384  supisoex  9385  eqinf  9395  infval  9397  infmo  9407  infpr  9415  infempty  9419  oieq1  9424  ordtypecbv  9429  ordtypelem7  9436  wemapsolem  9462  canthwdom  9491  zfregcl  9506  zfregclOLD  9507  elirrv  9509  elirrvOLD  9510  elirr  9511  noinfep  9578  cantnfp1lem3  9598  ttrcltr  9634  rankr1clem  9741  carden2b  9888  domtri2  9910  alephord3  9997  alephdom2  10006  alephval3  10029  dfac9  10056  kmlem2  10071  kmlem4  10073  isfin4  10216  isfin7  10220  fin23lem11  10236  isf32lem5  10276  isf34lem4  10296  fin1a2lem6  10324  fin1a2lem7  10325  fin1a2lem12  10330  itunisuc  10338  ac6n  10404  zorn2g  10422  zornn0g  10424  ttukeylem7  10434  infinfg  10485  axpowndlem3  10519  axpowndlem4  10520  axregnd  10524  elgch  10542  engch  10548  fpwwe2lem12  10562  fpwwe2  10563  pwfseqlem1  10578  pwfseqlem3  10580  hargch  10593  addnidpi  10821  pinq  10847  nqereu  10849  ltsonq  10889  prlem934  10953  ltexprlem7  10962  addcanpr  10966  prlem936  10967  reclem2pr  10968  reclem3pr  10969  supexpr  10974  ltsosr  11014  supsrlem  11031  axpre-lttri  11085  axpre-sup  11089  xrlenlt  11207  axlttri  11214  axsup  11218  ltne  11240  dedekind  11306  readdcan  11317  leadd1  11615  ltsub1  11643  ltsub2  11644  leord1  11674  lediv1  12018  lemuldiv  12033  lerec  12036  le2msq  12053  infm3  12112  suprnub  12118  infregelb  12137  avgle1  12414  avgle2  12415  znnnlt1  12551  indstr  12863  zsupss  12884  uzsupss  12887  rpneg  12973  xralrple  13154  xleneg  13167  xltadd1  13205  xposdif  13211  xmulneg1  13218  xltmul1  13241  xrsupexmnf  13254  xrinfmexpnf  13255  xrsupsslem  13256  xrinfmsslem  13257  xrub  13261  supxrleub  13275  infxrgelb  13285  difreicc  13434  nn0disj  13595  nelfzo  13616  elfznelfzo  13725  fvinim0ffz  13741  injresinjlem  13742  ssnn0fi  13944  leexp2  14130  exp11nnd  14220  hashbnd  14295  hasheni  14307  hashfundm  14401  hashbc  14412  wrdsymb0  14508  swrdnd  14614  swrdnd2  14615  pfxnd0  14648  repswswrd  14743  repswccat  14745  cshwidxmod  14762  cnpart  15199  sqrtlt  15220  limsuplt  15438  rlimrege0  15538  isercoll  15627  efle  16082  odd2np1  16307  sumodd  16354  divalglem7  16365  ndvdsadd  16376  fldivndvdslt  16382  bitsfval  16389  bitsval  16390  bits0  16394  bitsp1  16397  bitsmod  16402  bitscmp  16404  bitsinv1lem  16407  sadadd2lem2  16416  saddisjlem  16430  bitsshft  16441  gcdneg  16488  algcvgblem  16543  lcmneg  16569  isprm3  16649  dvdsnprmd  16656  isprm5  16674  rpexp  16689  phiprmpw  16743  m1dvdsndvds  16766  pythagtrip  16802  pcgcd1  16845  prmpwdvds  16872  prmreclem2  16885  prmreclem3  16886  prmreclem5  16888  prmreclem6  16889  vdwlem6  16954  vdwnnlem2  16964  vdwnnlem3  16965  vdwnn  16966  prmlem0  17073  prmlem1a  17074  divsfval  17508  mrisval  17593  ismri  17594  ismri2dad  17600  cidpropd  17673  cat1lem  18060  plttr  18303  joinval  18338  meetval  18352  acsfiindd  18516  isnsgrp  18688  smndex1n0mnd  18880  mgm2nsgrplem2  18887  sgrp2nmndlem3  18893  symgpssefmnd  19368  symgfix2  19388  pmtrdifellem4  19451  psgnunilem1  19465  psgnunilem5  19466  psgnunilem2  19467  psgnunilem3  19468  pmtrsn  19491  sylow1lem3  19572  sylow2alem2  19590  efgsfo  19711  ablfac1eulem  20046  ablfac1eu  20047  pgpfac1lem1  20048  pgpfac1lem5  20053  nzrunit  20498  zrninitoringc  20650  islbs  21069  lbsind  21073  lbspss  21075  lbspropd  21092  lspsnne1  21113  islbs2  21150  lbsacsbs  21152  lbsextlem1  21154  lbsextlem3  21156  lbsextlem4  21157  lbsextg  21158  frlmlbs  21793  islindf  21808  islinds2  21809  islindf2  21810  lindfind  21812  lindsind  21813  lindfrn  21817  lindfmm  21823  lsslindf  21826  islindf4  21834  opsrtoslem2  22050  psdmul  22148  cply1coe0  22282  cply1coe0bi  22283  mdetunilem7  22599  mdetunilem8  22600  mdetunilem9  22601  maducoeval2  22621  pmatcollpw3fi1lem1  22767  fvmptnn04ifa  22831  fvmptnn04ifc  22833  fvmptnn04ifd  22834  chfacffsupp  22837  chfacfscmul0  22839  chfacfpmmul0  22843  elcls  23054  maxlp  23128  perfi  23136  ordtbaslem  23169  ordtval  23170  ordtbas2  23172  ordtopn1  23175  ordtopn2  23176  ordtcnv  23182  ordtrest  23183  ordtrest2lem  23184  ordtrest2  23185  pnfnei  23201  mnfnei  23202  isreg2  23358  ordthauslem  23364  cmpfi  23389  cmpfii  23390  bwth  23391  nconnsubb  23404  hausdiag  23626  txkgen  23633  kqdisj  23713  ordthmeolem  23782  fbfinnfr  23822  trfbas  23825  fbunfip  23850  fbasrn  23865  trfil3  23869  ufileu  23900  fin1aufil  23913  hausflim  23962  alexsubALTlem2  24029  alexsubALTlem3  24030  alexsubALTlem4  24031  ptcmplem2  24034  ptcmplem3  24035  stdbdbl  24498  iccntr  24803  reconnlem2  24809  iccpnfcnv  24927  xrhmeo  24929  lebnumlem1  24944  lebnumlem2  24945  lebnumlem3  24946  bcthlem4  25310  minveclem3b  25411  ivthlem2  25435  ivthlem3  25436  mbfmax  25632  mbfposr  25635  i1fd  25664  mbfi1fseqlem4  25701  itg2splitlem  25731  itg2monolem1  25733  itg2cnlem1  25744  dvne0  25994  lhop1lem  25996  deg1nn0clb  26071  dgrle  26224  coemulhi  26235  aaliou3lem9  26333  cos11  26516  logleb  26586  argrege0  26594  logdivle  26605  ellogdm  26622  cxple  26678  cxplt2  26681  cxple3  26684  isosctrlem1  26801  atandm  26859  atans2  26914  atantayl2  26921  eldmgm  27005  ftalem7  27062  isppw2  27098  musum  27174  dchrsum2  27251  bposlem1  27267  lgsmod  27306  lgsdir2lem2  27309  lgsdir2  27313  lgsne0  27318  lgsprme0  27322  gausslemma2dlem4  27352  lgsquadlem1  27363  2lgslem3  27387  2lgsoddprm  27399  2sq2  27416  addsqrexnreu  27425  rpvmasumlem  27470  padicabv  27613  ostth3  27621  ostth  27622  noextenddif  27652  nodenselem4  27671  nodenselem5  27672  nodenselem7  27674  nolt02o  27679  nogt01o  27680  noresle  27681  nosupprefixmo  27684  noinfprefixmo  27685  nosupcbv  27686  nosupdm  27688  nosupfv  27690  nosupres  27691  nosupbnd1lem1  27692  nosupbnd1lem3  27694  nosupbnd1lem5  27696  nosupbnd1  27698  nosupbnd2lem1  27699  nosupbnd2  27700  noinfcbv  27701  noinfdm  27703  noinffv  27705  noinfres  27706  noinfbnd1lem1  27707  noinfbnd1lem3  27709  noinfbnd1lem5  27711  noinfbnd1  27713  noinfbnd2lem1  27714  noinfbnd2  27715  lenlts  27736  ltsne  27758  nocvxminlem  27766  lesrec  27811  eqcuts3  27816  cuteq1  27829  newbday  27914  ltslpss  27920  cofcutr  27936  lrrecfr  27955  addsval  27974  ltadds2  28003  lenegs  28058  lesubsubsbd  28098  lesubsubs2bd  28099  lesubsubs3bd  28100  lesubaddsd  28105  ltmuls2  28183  lemuls2d  28186  lemuls1d  28187  oncutlt  28276  onles  28280  pw2cut2  28474  bdaypw2bnd  28477  bdayfinbndlem1  28479  istrkgld  28547  axtgupdim2  28559  tglowdim2l  28738  axlowdimlem16  29046  axlowdim2  29049  axlowdim  29050  numedglnl  29233  usgredg2v  29316  lfuhgr1v0e  29343  cusgrfi  29548  vtxd0nedgb  29578  vtxduhgr0edgnel  29584  1loopgrnb0  29592  1hevtxdg0  29595  vtxdgoddnumeven  29643  wlkp1lem1  29761  wlkp1lem2  29762  wlkp1lem5  29765  dfpth2  29818  crctcsh  29913  clwlkclwwlklem2a4  30088  eupth2eucrct  30308  eupth2lem3lem3  30321  eupth2lem3lem4  30322  eupth2lem3lem6  30324  eupth2lem3lem7  30325  eupth2lems  30329  eupth2  30330  konigsberglem4  30346  nfrgr2v  30363  frgrwopreglem3  30405  fusgr2wsp2nb  30425  frgrreggt1  30484  friendshipgt3  30489  lpni  30572  nmobndseqi  30871  minvecolem5  30973  chpsscon3  31595  chnle  31606  nonbooli  31743  pjnel  31818  specval  31990  nmcfnlbi  32144  stri  32349  hstri  32357  cvbr  32374  cvcon3  32376  chcv1  32447  cvexchlem  32460  chrelat2  32462  nelun  32604  elpreq  32619  nelpr  32622  ifeqeqx  32633  nfpconfp  32726  suppiniseg  32780  isoun  32796  suppss3  32817  xrge0infss  32854  infxrge0gelb  32860  eliccelico  32871  elicoelioo  32872  nndiffz1  32880  hashgt1  32902  expgt0b  32911  nn0min  32915  ccatws1f1o  33032  toslublem  33053  tosglblem  33055  pmtrcnel  33171  cycpmco2  33215  isarchi2  33267  archiabl  33280  elrgspnlem2  33325  elrgspnlem3  33326  0nellinds  33451  lindssn  33459  lindfpropd  33463  ssdifidlprm  33539  mxidlirred  33553  ssmxidl  33555  esplyind  33740  lbslsat  33782  lindsunlem  33790  rtelextdg2lem  33892  constrsqrtcl  33945  ordtcnvNEW  34086  ordtrestNEW  34087  ordtrest2NEWlem  34088  ordtrest2NEW  34089  ordtconnlem1  34090  xrge0iifcnv  34099  esumpcvgval  34244  esum2d  34259  ddemeas  34402  omssubadd  34466  oddpwdc  34520  eulerpartlems  34526  eulerpartlemf  34536  eulerpartlemt  34537  eulerpartlemr  34540  eulerpartlemgvv  34542  eulerpartlemn  34547  ballotlemfc0  34659  ballotlemfcc  34660  ballotlem4  34665  ballotlemimin  34672  ballotlem7  34702  plymulx  34714  signsply0  34717  reprinfz1  34788  reprpmtf1o  34792  reprdifc  34793  hgt750lema  34823  hgt750leme  34824  istrkg2d  34832  bnj23  34883  bnj1185  34957  bnj1228  35175  bnj1388  35197  bnj1417  35205  nummin  35258  axnulg  35273  axprALT2  35275  fineqvnttrclselem1  35287  onvf1odlem2  35308  onvf1odlem3  35309  revwlk  35329  isacycgr  35349  acycgr0v  35352  prclisacycgr  35355  erdszelem10  35404  satf0n0  35582  fmlaomn0  35594  fmlasucdisj  35603  satfv1fvfmla1  35627  satefvfmla1  35629  ismfs  35753  mvtinf  35759  untelirr  35912  untsucf  35914  untangtr  35918  dfon2lem3  35987  dfon2lem4  35988  dfon2lem7  35991  dfon2lem9  35993  distel  36005  funpartfv  36149  dfrdg4  36155  nn0prpwlem  36526  nn0prpw  36527  limsucncmpi  36649  limsucncmp  36650  ordcmp  36651  weiunlem  36667  weiunfrlem  36668  weiunfr  36671  axtcond  36682  regsfromregtco  36742  regsfromsetind  36743  unblimceq0  36789  unbdqndv1  36790  bj-hbntbi  37023  bj-equsexvwd  37092  bj-cbvexdv  37129  bj-ru1  37272  bj-nuliota  37386  topdifinffinlem  37685  topdifinffin  37686  icorempo  37689  relowlpssretop  37702  finxpreclem2  37728  finxpreclem6  37734  wl-issetft  37929  wl-eujustlem1  37935  leceifl  37952  lindsadd  37956  lindsenlbs  37958  matunitlindflem1  37959  poimirlem16  37979  poimirlem17  37980  poimirlem18  37981  poimirlem19  37982  poimirlem21  37984  poimirlem23  37986  poimirlem26  37989  poimirlem27  37990  poimirlem28  37991  poimirlem31  37994  poimir  37996  mblfinlem2  38001  mblfinlem3  38002  ismblfin  38004  cnambfre  38011  itg2addnclem  38014  itg2addnclem2  38015  iblabsnclem  38026  ftc1anclem1  38036  areacirc  38056  heibor1lem  38152  heiborlem1  38154  heiborlem6  38159  heiborlem8  38161  heiborlem10  38163  smprngopr  38395  ecin0  38695  ax12inda  39416  riotaclbgBAD  39422  lcvfbr  39488  lcvbr  39489  lsatcv0  39499  l1cvpat  39522  opltcon3b  39672  cvrfval  39736  cvrval  39737  cvrnbtwn  39739  cvrval2  39742  cvrnbtwn2  39743  cvrnbtwn3  39744  cvrcon3b  39745  cvrnbtwn4  39747  atnlt  39781  iscvlat  39791  cvlexch1  39796  hlsuprexch  39849  hlrelat5N  39869  hlrelat2  39871  cvrval5  39883  3dimlem1  39926  3dim1lem5  39934  3dim2  39936  3dim3  39937  llnnlt  39991  islpln5  40003  lplni2  40005  lvolex3N  40006  lplnnle2at  40009  islpln2a  40016  lplnribN  40019  lplnexllnN  40032  lplnnlt  40033  lvoli3  40045  islvol5  40047  lvoli2  40049  lvolnle3at  40050  islvol2aN  40060  4atlem11  40077  lvolnltN  40086  dalawlem15  40353  4atexlemex2  40539  4atex  40544  4atex2-0aOLDN  40546  4atex2-0cOLDN  40548  lautcvr  40560  ltrnfset  40585  ltrnset  40586  ltrnu  40589  trlfset  40628  trlset  40629  trlval2  40631  cdlemd6  40671  cdleme0nex  40758  cdleme18d  40763  cdleme25b  40822  cdleme25cv  40826  cdleme29b  40843  cdleme31fv  40858  cdleme31fv2  40861  cdlemefrs29bpre0  40864  cdlemefr32sn2aw  40872  cdlemefr29bpre0N  40874  cdlemefr29clN  40875  cdlemefr32fvaN  40877  cdlemefr32fva1  40878  cdlemefs32sn1aw  40882  cdleme32fva  40905  cdleme32fvaw  40907  cdleme40v  40937  cdleme42b  40946  cdleme46f2g2  40961  cdleme46f2g1  40962  cdleme48gfv  41005  cdlemg1fvawlemN  41041  cdlemg1cex  41056  cdlemg6d  41089  cdlemm10N  41586  dicffval  41642  dicfval  41643  dicval  41644  dicfnN  41651  dicvalrelN  41653  dihffval  41698  dihfval  41699  dihlsscpre  41702  dvh4dimat  41906  dvh3dimatN  41907  dvh4dimlem  41911  dvh3dim  41914  dvh4dimN  41915  dvh3dim2  41916  dvh3dim3N  41917  mapdcv  42128  mapdh9aOLDN  42258  hdmapfval  42295  hdmapval  42296  hdmapval2  42300  hdmap11lem2  42310  dvrelog2b  42527  aks4d1p4  42540  aks4d1p5  42541  aks4d1p7  42544  aks4d1p8d2  42546  aks4d1p8  42548  aks4d1  42550  aks6d1c2p2  42580  hashnexinj  42589  rspcsbnea  42592  aks6d1c5  42600  aks6d1c6lem3  42633  aks6d1c7  42645  supinf  42703  oexpreposd  42776  mullt0b2d  42951  flt4lem7  43114  nna4b4nsq  43115  ellz1  43221  rencldnfilem  43274  jm2.22  43449  jm2.23  43450  wepwsolem  43496  fnwe2lem2  43505  aomclem8  43515  unxpwdom3  43549  onsupmaxb  43693  onexlimgt  43697  onsupeqnmax  43701  onov0suclim  43728  oaordnr  43750  omnord1  43759  oenord1  43770  oaomoencom  43771  oenass  43773  cantnfresb  43778  tfsnfin  43806  ralopabb  43864  nlimsuc  43894  ifpbi12  43941  dfsucon  43976  sqrtcvallem1  44084  ss2iundf  44112  frege124d  44214  clsk3nimkb  44493  clsk1indlem1  44498  clsk1independent  44499  ntrneineine1lem  44537  ntrneicls11  44543  clsneiel1  44561  clsneiel2  44562  neicvgel1  44572  neicvgel2  44573  radcnvrat  44767  rusbcALT  44891  en3lpVD  45297  0elaxnul  45436  omssaxinf2  45441  permaxnul  45461  permaxinf2lem  45465  nregmodel  45470  eliin2f  45560  nssd  45561  wessf1ornlem  45641  rexanuz2nf  45946  limsupre2lem  46178  icccncfext  46341  stoweidlem14  46468  stoweidlem34  46488  stoweidlem59  46513  etransclem24  46712  nnfoctbdjlem  46909  nnfoctbdj  46910  hspmbllem2  47081  nsssmfmbflem  47232  fsetsnprcnex  47523  eu2ndop1stv  47593  afvfv0bi  47620  afvco2  47644  ndmaovg  47652  ndfatafv2nrn  47689  afv2ndefb  47692  afv2fv0  47733  nelbr  47742  otiunsndisjX  47747  fun2dmnopgexmpl  47752  ltnltne  47767  readdcnnred  47771  resubcnnred  47772  recnmulnred  47773  cndivrenred  47774  ichnreuop  47952  nprmmul1  48007  fmtnoinf  48019  odz2prm2pw  48046  prmdvdsfmtnof1lem2  48068  lighneallem3  48090  lighneallem4  48093  requad1  48118  isodd3  48148  bits0ALTV  48175  nfermltl8rev  48238  nfermltl2rev  48239  nfermltlrev  48240  upgrimpths  48405  isubgr3stgrlem3  48464  usgrexmpl12ngric  48534  pgnbgreunbgrlem2lem1  48610  pgnbgreunbgrlem2lem2  48611  pgnbgreunbgrlem2lem3  48612  pgnbgreunbgrlem5lem1  48616  pgnbgreunbgrlem5lem2  48617  pgnbgreunbgrlem5lem3  48618  lgricngricex  48625  lidldomnnring  48732  ztprmneprm  48843  lindepsnlininds  48948  islindeps  48949  lindslinindsimp2lem5  48958  lindslinindsimp2  48959  line2ylem  49247  line2xlem  49249  map0cor  49350  nelsubc3lem  49565  fulltermc2  50007  setc1onsubc  50097  cnelsubclem  50098  elsetrecslem  50194