Theorem notbid 320

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 317	. . 3 ⊢ (𝜓 ↔ ¬ ¬ 𝜓)
3		notnotb 317	. . 3 ⊢ (𝜒 ↔ ¬ ¬ 𝜒)
4	1, 2, 3	3bitr3g 315	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 ↔ ¬ ¬ 𝜒))
5	4	con4bid 319	1 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  notbi  321  annotanannot  841  con3ALT  1091  xorbi12d  1533  equsexvw  2013  cbvexvw  2045  cbvexdvaw  2047  excomimw  2052  hbe1w  2058  19.8aw  2060  exexw  2061  ru0  2140  cbvexv1  2352  cbvex2v  2354  drex1v  2380  cbvex  2409  cbvex2  2422  drex1  2451  eujustALT  2578  necon3abid  2972  neleq12d  3045  cbvrexdva  3222  cbvrexfw  3282  cbvrexdva2  3318  cbvrexf  3327  cbvexeqsetf  3448  ceqsex  3480  ceqsexv  3481  gencbval  3491  spcegf  3531  spc2gv  3539  spc2d  3541  spc3gv  3543  ceqsralbv  3596  cdeqnot  3710  rru  3721  ruOLD  3723  sbcng  3771  sbcrext  3806  cbvrexcsf  3875  difjust  3886  eldif  3894  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  6074  poirr2  6080  cnvpo  6241  dfpo2  6250  predpoirr  6287  predfrirr  6288  frpomin  6294  nordeq  6332  ordtri1  6346  ordtri3  6349  fvmpti  6937  fndmdif  6986  rexrnmptw  7039  rexrnmpt  7041  rexima  7185  f1imapss  7213  f1ounsn  7219  cbvexfo  7237  nf1const  7251  soisoi  7275  isopolem  7292  weniso  7301  imaeqsalvOLD  7311  canth  7313  riotaclb  7357  rexrnmpo  7499  ndmovg  7542  sorpssuni  7678  sorpssint  7679  fr3nr  7718  dfwe2  7720  ordsucsssuc  7766  nlimsucg  7785  orduninsuc  7786  dfom2  7811  ssnlim  7829  resf1extb  7878  f1oweALT  7916  frxp  8068  poxp  8070  frxp2  8086  frxp3  8093  xpord3inddlem  8096  soseq  8101  suppofssd  8145  suppcoss  8149  smoword  8299  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  elirrvOLDOLD  9508  elirr  9509  noinfep  9576  cantnfp1lem3  9596  ttrcltr  9632  rankr1clem  9739  carden2b  9886  domtri2  9908  alephord3  9995  alephdom2  10004  alephval3  10027  dfac9  10054  kmlem2  10069  kmlem4  10071  isfin4  10215  isfin7  10219  fin23lem11  10235  isf32lem5  10275  isf34lem4  10295  fin1a2lem6  10323  fin1a2lem7  10324  fin1a2lem12  10329  itunisuc  10337  ac6n  10403  zorn2g  10421  zornn0g  10423  ttukeylem7  10433  infinfg  10484  axpowndlem3  10518  axpowndlem4  10519  axregnd  10523  elgch  10541  engch  10547  fpwwe2lem12  10561  fpwwe2  10562  pwfseqlem1  10577  pwfseqlem3  10579  hargch  10592  addnidpi  10820  pinq  10846  nqereu  10848  ltsonq  10888  prlem934  10952  ltexprlem7  10961  addcanpr  10965  prlem936  10966  reclem2pr  10967  reclem3pr  10968  supexpr  10973  ltsosr  11013  supsrlem  11030  axpre-lttri  11084  axpre-sup  11088  xrlenlt  11206  axlttri  11213  axsup  11217  ltne  11239  dedekind  11305  readdcan  11316  leadd1  11614  ltsub1  11642  ltsub2  11643  leord1  11673  lediv1  12016  lemuldiv  12031  lerec  12034  le2msq  12051  infm3  12110  suprnub  12116  infregelb  12135  avgle1  12412  avgle2  12413  znnnlt1  12549  indstr  12861  zsupss  12882  uzsupss  12885  rpneg  12971  xralrple  13152  xleneg  13165  xltadd1  13203  xposdif  13209  xmulneg1  13216  xltmul1  13239  xrsupexmnf  13252  xrinfmexpnf  13253  xrsupsslem  13254  xrinfmsslem  13255  xrub  13259  supxrleub  13273  infxrgelb  13283  difreicc  13432  nn0disj  13593  nelfzo  13614  elfznelfzo  13723  fvinim0ffz  13739  injresinjlem  13740  ssnn0fi  13942  leexp2  14128  exp11nnd  14218  hashbnd  14293  hasheni  14305  hashfundm  14399  hashbc  14410  wrdsymb0  14506  swrdnd  14612  swrdnd2  14613  pfxnd0  14646  repswswrd  14741  repswccat  14743  cshwidxmod  14760  cnpart  15197  sqrtlt  15218  limsuplt  15436  rlimrege0  15536  isercoll  15625  efle  16080  odd2np1  16305  sumodd  16352  divalglem7  16363  ndvdsadd  16374  fldivndvdslt  16380  bitsfval  16387  bitsval  16388  bits0  16392  bitsp1  16395  bitsmod  16400  bitscmp  16402  bitsinv1lem  16405  sadadd2lem2  16414  saddisjlem  16428  bitsshft  16439  gcdneg  16486  algcvgblem  16541  lcmneg  16567  isprm3  16647  dvdsnprmd  16654  isprm5  16672  rpexp  16687  phiprmpw  16741  m1dvdsndvds  16764  pythagtrip  16800  pcgcd1  16843  prmpwdvds  16870  prmreclem2  16883  prmreclem3  16884  prmreclem5  16886  prmreclem6  16887  vdwlem6  16952  vdwnnlem2  16962  vdwnnlem3  16963  vdwnn  16964  prmlem0  17071  prmlem1a  17072  divsfval  17506  mrisval  17591  ismri  17592  ismri2dad  17598  cidpropd  17671  cat1lem  18058  plttr  18301  joinval  18336  meetval  18350  acsfiindd  18514  isnsgrp  18686  smndex1n0mnd  18878  mgm2nsgrplem2  18885  sgrp2nmndlem3  18891  symgpssefmnd  19365  symgfix2  19385  pmtrdifellem4  19448  psgnunilem1  19462  psgnunilem5  19463  psgnunilem2  19464  psgnunilem3  19465  pmtrsn  19488  sylow1lem3  19569  sylow2alem2  19587  efgsfo  19708  ablfac1eulem  20043  ablfac1eu  20044  pgpfac1lem1  20045  pgpfac1lem5  20050  nzrunit  20499  zrninitoringc  20651  islbs  21069  lbsind  21073  lbspss  21075  lbspropd  21092  lspsnne1  21113  islbs2  21150  lbsacsbs  21152  lbsextlem1  21154  lbsextlem3  21156  lbsextlem4  21157  lbsextg  21158  frlmlbs  21775  islindf  21790  islinds2  21791  islindf2  21792  lindfind  21794  lindsind  21795  lindfrn  21799  lindfmm  21805  lsslindf  21808  islindf4  21816  opsrtoslem2  22035  psdmul  22157  cply1coe0  22290  cply1coe0bi  22291  mdetunilem7  22604  mdetunilem8  22605  mdetunilem9  22606  maducoeval2  22626  pmatcollpw3fi1lem1  22772  fvmptnn04ifa  22836  fvmptnn04ifc  22838  fvmptnn04ifd  22839  chfacffsupp  22842  chfacfscmul0  22844  chfacfpmmul0  22848  elcls  23059  maxlp  23133  perfi  23141  ordtbaslem  23174  ordtval  23175  ordtbas2  23177  ordtopn1  23180  ordtopn2  23181  ordtcnv  23187  ordtrest  23188  ordtrest2lem  23189  ordtrest2  23190  pnfnei  23206  mnfnei  23207  isreg2  23363  ordthauslem  23369  cmpfi  23394  cmpfii  23395  bwth  23396  nconnsubb  23409  hausdiag  23631  txkgen  23638  kqdisj  23718  ordthmeolem  23787  fbfinnfr  23827  trfbas  23830  fbunfip  23855  fbasrn  23870  trfil3  23874  ufileu  23905  fin1aufil  23918  hausflim  23967  alexsubALTlem2  24034  alexsubALTlem3  24035  alexsubALTlem4  24036  ptcmplem2  24039  ptcmplem3  24040  stdbdbl  24503  iccntr  24808  reconnlem2  24814  iccpnfcnv  24932  xrhmeo  24934  lebnumlem1  24949  lebnumlem2  24950  lebnumlem3  24951  bcthlem4  25315  minveclem3b  25416  ivthlem2  25440  ivthlem3  25441  mbfmax  25637  mbfposr  25640  i1fd  25669  mbfi1fseqlem4  25706  itg2splitlem  25736  itg2monolem1  25738  itg2cnlem1  25749  dvne0  25999  lhop1lem  26001  deg1nn0clb  26076  dgrle  26229  coemulhi  26240  aaliou3lem9  26337  cos11  26518  logleb  26588  argrege0  26596  logdivle  26607  ellogdm  26624  cxple  26680  cxplt2  26683  cxple3  26686  isosctrlem1  26803  atandm  26861  atans2  26916  atantayl2  26923  eldmgm  27006  ftalem7  27063  isppw2  27099  musum  27175  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  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  29547  vtxd0nedgb  29577  vtxduhgr0edgnel  29583  1loopgrnb0  29591  1hevtxdg0  29594  vtxdgoddnumeven  29642  wlkp1lem1  29760  wlkp1lem2  29761  wlkp1lem5  29764  dfpth2  29817  crctcsh  29912  clwlkclwwlklem2a4  30087  eupth2eucrct  30307  eupth2lem3lem3  30320  eupth2lem3lem4  30321  eupth2lem3lem6  30323  eupth2lem3lem7  30324  eupth2lems  30328  eupth2  30329  konigsberglem4  30345  nfrgr2v  30362  frgrwopreglem3  30404  fusgr2wsp2nb  30424  frgrreggt1  30483  friendshipgt3  30488  lpni  30571  nmobndseqi  30870  minvecolem5  30972  chpsscon3  31594  chnle  31605  nonbooli  31742  pjnel  31817  specval  31989  nmcfnlbi  32143  stri  32348  hstri  32356  cvbr  32373  cvcon3  32375  chcv1  32446  cvexchlem  32459  chrelat2  32461  nelun  32603  elpreq  32618  nelpr  32621  ifeqeqx  32632  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  33172  cycpmco2  33216  isarchi2  33268  archiabl  33281  elrgspnlem2  33326  elrgspnlem3  33327  0nellinds  33455  lindssn  33463  lindfpropd  33467  ssdifidlprm  33543  mxidlirred  33557  ssmxidl  33559  dflringlem  33587  esplyind  33769  lbslsat  33810  lindsunlem  33818  rtelextdg2lem  33920  constrsqrtcl  33973  ordtcnvNEW  34114  ordtrestNEW  34115  ordtrest2NEWlem  34116  ordtrest2NEW  34117  ordtconnlem1  34118  xrge0iifcnv  34127  esumpcvgval  34272  esum2d  34287  ddemeas  34430  omssubadd  34494  oddpwdc  34548  eulerpartlems  34554  eulerpartlemf  34564  eulerpartlemt  34565  eulerpartlemr  34568  eulerpartlemgvv  34570  eulerpartlemn  34575  ballotlemfc0  34687  ballotlemfcc  34688  ballotlem4  34693  ballotlemimin  34700  ballotlem7  34730  plymulx  34742  signsply0  34745  reprinfz1  34816  reprpmtf1o  34820  reprdifc  34821  hgt750lema  34851  hgt750leme  34852  istrkg2d  34860  bnj23  34914  bnj1185  34988  bnj1228  35206  bnj1388  35228  bnj1417  35236  nummin  35287  axprALT2  35303  fineqvnttrclselem1  35315  axnulg  35339  onvf1odlem2  35345  onvf1odlem3  35346  revwlk  35366  isacycgr  35386  acycgr0v  35389  prclisacycgr  35392  erdszelem10  35441  satf0n0  35619  fmlaomn0  35631  fmlasucdisj  35640  satfv1fvfmla1  35664  satefvfmla1  35666  ismfs  35790  mvtinf  35796  untelirr  35949  untsucf  35951  untangtr  35955  dfon2lem3  36024  dfon2lem4  36025  dfon2lem7  36028  dfon2lem9  36030  distel  36042  funpartfv  36186  dfrdg4  36192  nn0prpwlem  36563  nn0prpw  36564  limsucncmpi  36686  limsucncmp  36687  ordcmp  36688  weiunlem  36704  weiunfrlem  36705  weiunfr  36708  axtcond  36719  regsfromregtco  36779  regsfromsetind  36780  unblimceq0  36826  unbdqndv1  36827  bj-hbntbi  37060  bj-equsexvwd  37129  bj-cbvexdv  37166  bj-ru1  37309  bj-nuliota  37423  topdifinffinlem  37722  topdifinffin  37723  icorempo  37726  relowlpssretop  37739  finxpreclem2  37765  finxpreclem6  37771  wl-issetft  37966  wl-eujustlem1  37972  leceifl  37989  lindsadd  37993  lindsenlbs  37995  matunitlindflem1  37996  poimirlem16  38016  poimirlem17  38017  poimirlem18  38018  poimirlem19  38019  poimirlem21  38021  poimirlem23  38023  poimirlem26  38026  poimirlem27  38027  poimirlem28  38028  poimirlem31  38031  poimir  38033  mblfinlem2  38038  mblfinlem3  38039  ismblfin  38041  cnambfre  38048  itg2addnclem  38051  itg2addnclem2  38052  iblabsnclem  38063  ftc1anclem1  38073  areacirc  38093  heibor1lem  38189  heiborlem1  38191  heiborlem6  38196  heiborlem8  38198  heiborlem10  38200  smprngopr  38432  ecin0  38732  ax12inda  39453  riotaclbgBAD  39459  lcvfbr  39525  lcvbr  39526  lsatcv0  39536  l1cvpat  39559  opltcon3b  39709  cvrfval  39773  cvrval  39774  cvrnbtwn  39776  cvrval2  39779  cvrnbtwn2  39780  cvrnbtwn3  39781  cvrcon3b  39782  cvrnbtwn4  39784  atnlt  39818  iscvlat  39828  cvlexch1  39833  hlsuprexch  39886  hlrelat5N  39906  hlrelat2  39908  cvrval5  39920  3dimlem1  39963  3dim1lem5  39971  3dim2  39973  3dim3  39974  llnnlt  40028  islpln5  40040  lplni2  40042  lvolex3N  40043  lplnnle2at  40046  islpln2a  40053  lplnribN  40056  lplnexllnN  40069  lplnnlt  40070  lvoli3  40082  islvol5  40084  lvoli2  40086  lvolnle3at  40087  islvol2aN  40097  4atlem11  40114  lvolnltN  40123  dalawlem15  40390  4atexlemex2  40576  4atex  40581  4atex2-0aOLDN  40583  4atex2-0cOLDN  40585  lautcvr  40597  ltrnfset  40622  ltrnset  40623  ltrnu  40626  trlfset  40665  trlset  40666  trlval2  40668  cdlemd6  40708  cdleme0nex  40795  cdleme18d  40800  cdleme25b  40859  cdleme25cv  40863  cdleme29b  40880  cdleme31fv  40895  cdleme31fv2  40898  cdlemefrs29bpre0  40901  cdlemefr32sn2aw  40909  cdlemefr29bpre0N  40911  cdlemefr29clN  40912  cdlemefr32fvaN  40914  cdlemefr32fva1  40915  cdlemefs32sn1aw  40919  cdleme32fva  40942  cdleme32fvaw  40944  cdleme40v  40974  cdleme42b  40983  cdleme46f2g2  40998  cdleme46f2g1  40999  cdleme48gfv  41042  cdlemg1fvawlemN  41078  cdlemg1cex  41093  cdlemg6d  41126  cdlemm10N  41623  dicffval  41679  dicfval  41680  dicval  41681  dicfnN  41688  dicvalrelN  41690  dihffval  41735  dihfval  41736  dihlsscpre  41739  dvh4dimat  41943  dvh3dimatN  41944  dvh4dimlem  41948  dvh3dim  41951  dvh4dimN  41952  dvh3dim2  41953  dvh3dim3N  41954  mapdcv  42165  mapdh9aOLDN  42295  hdmapfval  42332  hdmapval  42333  hdmapval2  42337  hdmap11lem2  42347  dvrelog2b  42564  aks4d1p4  42577  aks4d1p5  42578  aks4d1p7  42581  aks4d1p8d2  42583  aks4d1p8  42585  aks4d1  42587  aks6d1c2p2  42617  hashnexinj  42626  rspcsbnea  42629  aks6d1c5  42637  aks6d1c6lem3  42670  aks6d1c7  42682  supinf  42739  oexpreposd  42812  mullt0b2d  42987  flt4lem7  43122  nna4b4nsq  43123  ellz1  43229  rencldnfilem  43278  jm2.22  43453  jm2.23  43454  wepwsolem  43500  fnwe2lem2  43509  aomclem8  43519  unxpwdom3  43553  onsupmaxb  43697  onexlimgt  43701  onsupeqnmax  43705  onov0suclim  43732  oaordnr  43754  omnord1  43763  oenord1  43774  oaomoencom  43775  oenass  43777  cantnfresb  43782  tfsnfin  43810  ralopabb  43868  nlimsuc  43898  ifpbi12  43945  dfsucon  43980  sqrtcvallem1  44088  ss2iundf  44116  frege124d  44218  clsk3nimkb  44497  clsk1indlem1  44502  clsk1independent  44503  ntrneineine1lem  44541  ntrneicls11  44547  clsneiel1  44565  clsneiel2  44566  neicvgel1  44576  neicvgel2  44577  radcnvrat  44771  rusbcALT  44895  en3lpVD  45301  0elaxnul  45440  omssaxinf2  45445  permaxnul  45465  permaxinf2lem  45469  nregmodel  45474  eliin2f  45563  nssd  45564  wessf1ornlem  45644  rexanuz2nf  45947  limsupre2lem  46179  icccncfext  46342  stoweidlem14  46469  stoweidlem34  46489  stoweidlem59  46514  etransclem24  46713  nnfoctbdjlem  46910  nnfoctbdj  46911  hspmbllem2  47082  nsssmfmbflem  47233  fsetsnprcnex  47530  eu2ndop1stv  47600  afvfv0bi  47627  afvco2  47651  ndmaovg  47659  ndfatafv2nrn  47696  afv2ndefb  47699  afv2fv0  47740  nelbr  47749  otiunsndisjX  47754  fun2dmnopgexmpl  47759  ltnltne  47774  readdcnnred  47778  resubcnnred  47779  recnmulnred  47780  cndivrenred  47781  ichnreuop  47959  nprmmul1  48014  fmtnoinf  48026  odz2prm2pw  48053  prmdvdsfmtnof1lem2  48075  lighneallem3  48097  lighneallem4  48100  requad1  48125  isodd3  48155  bits0ALTV  48182  nfermltl8rev  48245  nfermltl2rev  48246  nfermltlrev  48247  upgrimpths  48412  isubgr3stgrlem3  48471  usgrexmpl12ngric  48541  pgnbgreunbgrlem2lem1  48617  pgnbgreunbgrlem2lem2  48618  pgnbgreunbgrlem2lem3  48619  pgnbgreunbgrlem5lem1  48623  pgnbgreunbgrlem5lem2  48624  pgnbgreunbgrlem5lem3  48625  lgricngricex  48632  lidldomnnring  48739  ztprmneprm  48850  lindepsnlininds  48955  islindeps  48956  lindslinindsimp2lem5  48965  lindslinindsimp2  48966  line2ylem  49254  line2xlem  49256  map0cor  49357  nelsubc3lem  49572  fulltermc2  50014  setc1onsubc  50104  cnelsubclem  50105  elsetrecslem  50201