Theorem notbid 321

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  notbi  322  annotanannot  848  con3ALT  1101  xorbi12d  1555  equsexvw  2038  cbvexvw  2070  cbvexdvaw  2072  excomimw  2077  hbe1w  2083  19.8aw  2085  exexw  2086  ru0  2164  cbvexv1  2373  cbvex2v  2375  drex1v  2401  cbvex  2430  cbvex2  2443  drex1  2472  eujustALT  2599  necon3abid  2993  neleq12d  3068  cbvrexdva  3245  cbvrexfw  3305  cbvrexdva2  3339  cbvrexf  3348  cbvexeqsetf  3468  ceqsex  3500  ceqsexv  3501  gencbval  3511  spcegf  3549  spc2gv  3557  spc2d  3559  spc3gv  3561  ceqsralbv  3614  cdeqnot  3729  rru  3740  sbcng  3789  sbcrext  3823  cbvrexcsf  3893  difjust  3904  eldif  3912  dfpss3  4040  difeq2  4071  disjne  4411  pssdifcom1  4448  eldifpr  4622  rexsng  4640  elpwunsn  4648  eldiftp  4651  rexprg  4661  preqsnd  4822  disjxun  5105  exnelv  5274  nalsetOLD  5276  dtruALT2  5339  dtruALT  5357  rexxfrd  5378  rexxfr2d  5380  rexxfrd2  5382  rexxfr  5385  opthneg  5461  snopeqop  5487  otiunsndisj  5501  poeq1  5570  pocl  5575  swopo  5578  sotric  5597  sotrieq  5598  isso2i  5604  somo  5606  freq1  5626  frirr  5635  fr2nr  5636  frminex  5638  tz7.2  5642  wereu2  5656  poinxp  5740  frinxp  5742  posn  5745  frsn  5747  rexiunxp  5824  rexxpf  5831  intirr  6116  poirr2  6122  cnvpo  6289  dfpo2  6298  predpoirr  6335  predfrirr  6336  frpomin  6342  nordeq  6380  ordtri1  6395  ordtri3  6398  fvmpti  6989  fndmdif  7038  rexrnmptw  7091  rexrnmpt  7093  rexima  7240  f1imapss  7266  f1ounsn  7276  cbvexfo  7294  nf1const  7308  soisoi  7332  isopolem  7349  weniso  7360  canth  7370  riotaclb  7414  rexrnmpo  7556  ndmovg  7600  sorpssuni  7736  sorpssint  7737  fr3nr  7774  dfwe2  7776  ordsucsssuc  7822  nlimsucg  7841  orduninsuc  7842  dfom2  7867  ssnlim  7885  resf1extb  7934  f1oweALT  7972  frxp  8127  poxp  8129  frxp2  8145  frxp3  8152  xpord3inddlem  8155  soseq  8160  suppofssd  8204  suppcoss  8208  smoword  8358  tz7.48lem  8433  oacan  8538  oaword  8539  omlimcl  8568  omeulem1  8572  nnaword  8618  nnmword  8624  nneob  8647  naddss1  8681  brdifun  8730  swoer  8731  undifixp  8944  boxcutc  8951  2dom  9040  php  9204  phpeqd  9209  nndomog  9210  onomeneq  9211  nnsdomo  9216  unxpdomlem2  9230  frfi  9258  unfilem1  9278  tfsnfin2  9333  supeq3  9422  supeq123d  9423  supmo  9425  eqsup  9429  supub  9432  sup0  9440  suppr  9445  supisolem  9447  supisoex  9448  eqinf  9458  infval  9460  infmo  9470  infpr  9478  infempty  9482  oieq1  9487  ordtypecbv  9492  ordtypelem7  9499  wemapsolem  9525  canthwdom  9554  zfregcl  9569  zfregclOLD  9570  elirrv  9572  elirrvOLD  9573  elirrvOLDOLD  9574  elirr  9575  noinfep  9642  cantnfp1lem3  9662  ttrcltr  9698  rankr1clem  9805  carden2b  9975  domtri2  9997  alephord3  10084  alephdom2  10093  alephval3  10116  dfac9  10142  kmlem2  10157  kmlem4  10159  isfin4  10302  isfin7  10306  fin23lem11  10322  isf32lem5  10362  isf34lem4  10382  fin1a2lem6  10410  fin1a2lem7  10411  fin1a2lem12  10416  itunisuc  10424  ac6n  10490  zorn2g  10508  zornn0g  10510  ttukeylem7  10520  infinfg  10575  axpowndlem3  10609  axpowndlem4  10610  axregnd  10614  elgch  10632  engch  10638  fpwwe2lem12  10652  fpwwe2  10653  pwfseqlem1  10668  pwfseqlem3  10670  hargch  10683  addnidpi  10911  pinq  10937  nqereu  10939  ltsonq  10979  prlem934  11043  ltexprlem7  11052  addcanpr  11056  prlem936  11057  reclem2pr  11058  reclem3pr  11059  supexpr  11064  ltsosr  11104  supsrlem  11121  axpre-lttri  11175  axpre-sup  11179  xrlenlt  11299  axlttri  11306  axsup  11310  ltne  11332  dedekind  11398  readdcan  11409  leadd1  11707  ltsub1  11735  ltsub2  11736  leord1  11766  lediv1  12105  lemuldiv  12120  lerec  12123  le2msq  12140  infm3  12199  suprnub  12205  infregelb  12224  avgle1  12509  avgle2  12510  znnnlt1  12646  indstr  12966  zsupss  12987  uzsupss  12990  rpneg  13076  xralrple  13257  xleneg  13270  xltadd1  13308  xposdif  13314  xmulneg1  13321  xltmul1  13344  xrsupexmnf  13357  xrinfmexpnf  13358  xrsupsslem  13359  xrinfmsslem  13360  xrub  13364  supxrleub  13378  infxrgelb  13388  difreicc  13537  nn0disj  13699  nelfzo  13720  elfznelfzo  13829  fvinim0ffz  13845  injresinjlem  13846  ssnn0fi  14049  leexp2  14235  exp11nnd  14325  hashbnd  14400  hasheni  14412  hashfundm  14507  hashbc  14518  wrdsymb0  14614  swrdnd  14724  swrdnd2  14725  pfxnd0  14758  repswswrd  14855  repswccat  14857  cshwidxmod  14874  cnpart  15327  sqrtlt  15348  limsuplt  15566  rlimrege0  15666  isercoll  15755  efle  16208  odd2np1  16433  sumodd  16480  divalglem7  16491  ndvdsadd  16502  fldivndvdslt  16508  bitsfval  16515  bitsval  16516  bits0  16520  bitsp1  16523  bitsmod  16528  bitscmp  16530  bitsinv1lem  16533  sadadd2lem2  16542  saddisjlem  16556  bitsshft  16567  gcdneg  16614  algcvgblem  16669  lcmneg  16695  isprm3  16775  dvdsnprmd  16782  isprm5  16800  rpexp  16815  phiprmpw  16869  m1dvdsndvds  16892  pythagtrip  16928  pcgcd1  16971  prmpwdvds  16998  prmreclem2  17011  prmreclem3  17012  prmreclem5  17014  prmreclem6  17015  vdwlem6  17080  vdwnnlem2  17090  vdwnnlem3  17091  vdwnn  17092  prmlem0  17199  prmlem1a  17200  divsfval  17635  mrisval  17720  ismri  17721  ismri2dad  17727  cidpropd  17800  cat1lem  18187  plttr  18430  joinval  18465  meetval  18479  acsfiindd  18643  isnsgrp  18825  smndex1n0mnd  19023  mgm2nsgrplem2  19030  sgrp2nmndlem3  19036  degenmgm2nfun  19051  symgpssefmnd  19522  symgfix2  19542  pmtrdifellem4  19605  psgnunilem1  19619  psgnunilem5  19620  psgnunilem2  19621  psgnunilem3  19622  pmtrsn  19645  sylow1lem3  19726  sylow2alem2  19744  efgsfo  19865  ablfac1eulem  20200  ablfac1eu  20201  pgpfac1lem1  20202  pgpfac1lem5  20207  nzrunit  20684  zrninitoringc  20837  islbs  21259  lbsind  21263  lbspss  21265  lbspropd  21282  lspsnne1  21303  islbs2  21340  lbsacsbs  21342  lbsextlem1  21344  lbsextlem3  21346  lbsextlem4  21347  lbsextg  21348  ssdifidlprm  21548  frlmlbs  22009  islindf  22024  islinds2  22025  islindf2  22026  lindfind  22028  lindsind  22029  lindfrn  22033  lindfmm  22039  lsslindf  22042  islindf4  22050  lindsenlbs  22063  opsrtoslem2  22271  psdmul  22393  cply1coe0  22525  cply1coe0bi  22526  mdetunilem7  22839  mdetunilem8  22840  mdetunilem9  22841  maducoeval2  22861  matunitlindflem1  22900  pmatcollpw3fi1lem1  23010  fvmptnn04ifa  23074  fvmptnn04ifc  23076  fvmptnn04ifd  23077  chfacffsupp  23080  chfacfscmul0  23082  chfacfpmmul0  23086  elcls  23297  maxlp  23371  perfi  23379  ordtbaslem  23412  ordtval  23413  ordtbas2  23415  ordtopn1  23418  ordtopn2  23419  ordtcnv  23425  ordtrest  23426  ordtrest2lem  23427  ordtrest2  23428  pnfnei  23444  mnfnei  23445  isreg2  23601  ordthauslem  23607  cmpfi  23632  cmpfii  23633  bwth  23634  nconnsubb  23647  hausdiag  23870  txkgen  23877  kqdisj  23957  ordthmeolem  24026  fbfinnfr  24066  trfbas  24069  fbunfip  24094  fbasrn  24109  trfil3  24113  ufileu  24144  fin1aufil  24157  hausflim  24206  alexsubALTlem2  24273  alexsubALTlem3  24274  alexsubALTlem4  24275  ptcmplem2  24278  ptcmplem3  24279  stdbdbl  24742  iccntr  25047  reconnlem2  25053  iccpnfcnv  25171  xrhmeo  25173  lebnumlem1  25188  lebnumlem2  25189  lebnumlem3  25190  bcthlem4  25554  minveclem3b  25655  ivthlem2  25679  ivthlem3  25680  mbfmax  25876  mbfposr  25879  i1fd  25908  mbfi1fseqlem4  25945  itg2splitlem  25975  itg2monolem1  25977  itg2cnlem1  25988  dvne0  26238  lhop1lem  26240  deg1nn0clb  26315  dgrle  26468  coemulhi  26479  plymulidp  26511  aaliou3lem9  26581  cos11  26766  logleb  26836  argrege0  26844  logdivle  26855  ellogdm  26872  cxple  26928  cxplt2  26931  cxple3  26934  isosctrlem1  27051  atandm  27109  atans2  27164  atantayl2  27171  eldmgm  27254  ftalem7  27311  isppw2  27347  musum  27423  dchrsum2  27500  bposlem1  27516  lgsmod  27555  lgsdir2lem2  27558  lgsdir2  27562  lgsne0  27567  lgsprme0  27571  gausslemma2dlem4  27601  lgsquadlem1  27612  2lgslem3  27636  2lgsoddprm  27648  2sq2  27665  addsqrexnreu  27674  rpvmasumlem  27719  padicabv  27862  ostth3  27870  ostth  27871  noextenddif  27900  nodenselem4  27919  nodenselem5  27920  nodenselem7  27922  nolt02o  27927  nogt01o  27928  noresle  27929  nosupprefixmo  27932  noinfprefixmo  27933  nosupcbv  27934  nosupdm  27936  nosupfv  27938  nosupres  27939  nosupbnd1lem1  27940  nosupbnd1lem3  27942  nosupbnd1lem5  27944  nosupbnd1  27946  nosupbnd2lem1  27947  nosupbnd2  27948  noinfcbv  27949  noinfdm  27951  noinffv  27953  noinfres  27954  noinfbnd1lem1  27955  noinfbnd1lem3  27957  noinfbnd1lem5  27959  noinfbnd1  27961  noinfbnd2lem1  27962  noinfbnd2  27963  lenlts  27984  ltsne  28006  nocvxminlem  28015  lesrec  28060  eqcuts3  28065  cuteq1  28078  newbday  28163  ltslpss  28169  cofcutr  28185  lrrecfr  28204  addsval  28223  ltadds2  28252  lenegs  28307  lesubsubsbd  28347  lesubsubs2bd  28348  lesubsubs3bd  28349  lesubaddsd  28354  ltmuls2  28432  lemuls2d  28435  lemuls1d  28436  oncutlt  28525  onles  28529  pw2cut2  28723  bdaypw2bnd  28726  bdayfinbndlem1  28728  istrkgld  28796  axtgupdim2  28808  tglowdim2l  28994  axlowdimlem16  29398  axlowdim2  29401  axlowdim  29402  numedglnl  29585  usgredg2v  29671  lfuhgr1v0e  29698  cusgrfi  29902  vtxd0nedgb  29932  vtxduhgr0edgnel  29938  1loopgrnb0  29946  1hevtxdg0  29949  vtxdgoddnumeven  29997  wlkp1lem1  30115  wlkp1lem2  30116  wlkp1lem5  30119  revwlk  30130  dfpth2  30177  crctcsh  30276  clwlkclwwlklem2a4  30451  isacycgr  30614  eupth2eucrct  30681  eupth2lem3lem3  30694  eupth2lem3lem4  30695  eupth2lem3lem6  30697  eupth2lem3lem7  30698  eupth2lems  30702  eupth2  30703  konigsberglem4  30719  nfrgr2v  30736  frgrwopreglem3  30778  fusgr2wsp2nb  30798  frgrreggt1  30857  friendshipgt3  30862  lpni  30945  nmobndseqi  31244  minvecolem5  31346  chpsscon3  31968  chnle  31979  nonbooli  32116  pjnel  32191  specval  32363  nmcfnlbi  32517  stri  32722  hstri  32730  cvbr  32747  cvcon3  32749  chcv1  32820  cvexchlem  32833  chrelat2  32835  nelun  32972  elpreq  32987  nelpr  32990  ifeqeqx  33001  nfpconfp  33090  suppiniseg  33143  isoun  33159  suppss3  33179  xrge0infss  33216  infxrge0gelb  33222  eliccelico  33233  elicoelioo  33234  nndiffz1  33242  hashgt1  33264  expgt0b  33272  nn0min  33276  ccatws1f1o  33378  toslublem  33397  tosglblem  33399  pmtrcnel  33514  cycpmco2  33558  isarchi2  33610  archiabl  33623  elrgspnlem2  33668  elrgspnlem3  33669  0nellinds  33790  lindssn  33796  lindfpropd  33800  mxidlirred  33860  ssmxidl  33862  dflringlem  33889  esplyind  34070  lbslsat  34111  lindsunlem  34119  rtelextdg2lem  34221  constrsqrtcl  34274  ordtcnvNEW  34415  ordtrestNEW  34416  ordtrest2NEWlem  34417  ordtrest2NEW  34418  ordtconnlem1  34419  xrge0iifcnv  34428  esumpcvgval  34573  esum2d  34588  ddemeas  34732  omssubadd  34796  oddpwdc  34850  eulerpartlems  34856  eulerpartlemf  34866  eulerpartlemt  34867  eulerpartlemr  34870  eulerpartlemgvv  34872  eulerpartlemn  34877  ballotlemfc0  34989  ballotlemfcc  34990  ballotlem4  34995  ballotlemimin  35002  ballotlem7  35032  signsply0  35044  reprinfz1  35115  reprpmtf1o  35119  reprdifc  35120  hgt750lema  35150  hgt750leme  35151  istrkg2d  35159  bnj23  35213  bnj1185  35287  bnj1228  35505  bnj1388  35527  bnj1417  35535  ordtypeon  35580  nummin  35583  axprALT2  35602  fineqvnttrclselem1  35632  axnulg  35656  onvf1odlem2  35686  onvf1odlem3  35687  acycgr0v  35712  prclisacycgr  35715  erdszelem10  35764  satf0n0  35942  fmlaomn0  35954  fmlasucdisj  35963  satfv1fvfmla1  35987  satefvfmla1  35989  ismfs  36113  mvtinf  36119  untelirr  36272  untsucf  36274  untangtr  36278  dfon2lem3  36347  dfon2lem4  36348  dfon2lem7  36351  dfon2lem9  36353  distel  36365  funpartfv  36509  dfrdg4  36515  nmulprop  36755  naddle  36784  nn0prpwlem  36926  nn0prpw  36927  limsucncmpi  37049  limsucncmp  37050  ordcmp  37051  weiunlem  37067  weiunfrlem  37068  weiunfr  37071  axtcond  37082  regsfromregtco  37142  regsfromsetind  37143  unblimceq0  37189  unbdqndv1  37190  bj-hbntbi  37422  bj-equsexvwd  37491  bj-cbvexdv  37528  bj-ru1  37672  bj-nuliota  37786  topdifinffinlem  38086  topdifinffin  38087  icorempo  38090  relowlpssretop  38103  finxpreclem2  38129  finxpreclem6  38135  wl-issetft  38330  wl-eujustlem1  38336  leceifl  38348  lindsadd  38352  poimirlem16  38370  poimirlem17  38371  poimirlem18  38372  poimirlem19  38373  poimirlem21  38375  poimirlem23  38377  poimirlem26  38380  poimirlem27  38381  poimirlem28  38382  poimirlem31  38385  poimir  38387  mblfinlem2  38392  mblfinlem3  38393  ismblfin  38395  cnambfre  38402  itg2addnclem  38405  itg2addnclem2  38406  iblabsnclem  38417  ftc1anclem1  38427  areacirc  38447  heibor1lem  38544  heiborlem1  38546  heiborlem6  38551  heiborlem8  38553  heiborlem10  38555  smprngopr  38787  ecin0  39085  ax12inda  39806  riotaclbgBAD  39812  lcvfbr  39878  lcvbr  39879  lsatcv0  39889  l1cvpat  39912  opltcon3b  40062  cvrfval  40126  cvrval  40127  cvrnbtwn  40129  cvrval2  40132  cvrnbtwn2  40133  cvrnbtwn3  40134  cvrcon3b  40135  cvrnbtwn4  40137  atnlt  40171  iscvlat  40181  cvlexch1  40186  hlsuprexch  40239  hlrelat5N  40259  hlrelat2  40261  cvrval5  40273  3dimlem1  40316  3dim1lem5  40324  3dim2  40326  3dim3  40327  llnnlt  40381  islpln5  40393  lplni2  40395  lvolex3N  40396  lplnnle2at  40399  islpln2a  40406  lplnribN  40409  lplnexllnN  40422  lplnnlt  40423  lvoli3  40435  islvol5  40437  lvoli2  40439  lvolnle3at  40440  islvol2aN  40450  4atlem11  40467  lvolnltN  40476  dalawlem15  40743  4atexlemex2  40929  4atex  40934  4atex2-0aOLDN  40936  4atex2-0cOLDN  40938  lautcvr  40950  ltrnfset  40975  ltrnset  40976  ltrnu  40979  trlfset  41018  trlset  41019  trlval2  41021  cdlemd6  41061  cdleme0nex  41148  cdleme18d  41153  cdleme25b  41212  cdleme25cv  41216  cdleme29b  41233  cdleme31fv  41248  cdleme31fv2  41251  cdlemefrs29bpre0  41254  cdlemefr32sn2aw  41262  cdlemefr29bpre0N  41264  cdlemefr29clN  41265  cdlemefr32fvaN  41267  cdlemefr32fva1  41268  cdlemefs32sn1aw  41272  cdleme32fva  41295  cdleme32fvaw  41297  cdleme40v  41327  cdleme42b  41336  cdleme46f2g2  41351  cdleme46f2g1  41352  cdleme48gfv  41395  cdlemg1fvawlemN  41431  cdlemg1cex  41446  cdlemg6d  41479  cdlemm10N  41976  dicffval  42032  dicfval  42033  dicval  42034  dicfnN  42041  dicvalrelN  42043  dihffval  42088  dihfval  42089  dihlsscpre  42092  dvh4dimat  42296  dvh3dimatN  42297  dvh4dimlem  42301  dvh3dim  42304  dvh4dimN  42305  dvh3dim2  42306  dvh3dim3N  42307  mapdcv  42518  mapdh9aOLDN  42648  hdmapfval  42685  hdmapval  42686  hdmapval2  42690  hdmap11lem2  42700  dvrelog2b  42917  aks4d1p4  42930  aks4d1p5  42931  aks4d1p7  42934  aks4d1p8d2  42936  aks4d1p8  42938  aks4d1  42940  aks6d1c2p2  42970  hashnexinj  42979  rspcsbnea  42982  aks6d1c5  42990  aks6d1c6lem3  43023  aks6d1c7  43035  supinf  43094  oexpreposd  43182  mullt0b2d  43357  flt4lem7  43490  nna4b4nsq  43491  ellz1  43597  rencldnfilem  43646  jm2.22  43821  jm2.23  43822  wepwsolem  43868  fnwe2lem2  43877  aomclem8  43887  unxpwdom3  43921  onsupmaxb  44065  onexlimgt  44069  onsupeqnmax  44073  onov0suclim  44100  oaordnr  44122  omnord1  44131  oenord1  44142  oaomoencom  44143  oenass  44145  cantnfresb  44150  tfsnfin  44178  ralopabb  44236  nlimsuc  44266  ifpbi12  44313  dfsucon  44348  sqrtcvallem1  44456  ss2iundf  44484  frege124d  44586  clsk3nimkb  44865  clsk1indlem1  44870  clsk1independent  44871  ntrneineine1lem  44909  ntrneicls11  44915  clsneiel1  44933  clsneiel2  44934  neicvgel1  44944  neicvgel2  44945  radcnvrat  45123  rusbcALT  45247  en3lpVD  45652  0elaxnul  45791  omssaxinf2  45796  permaxnul  45816  permaxinf2lem  45820  nregmodel  45825  eliin2f  45921  nssd  45922  wessf1ornlem  46002  rexanuz2nf  46305  limsupre2lem  46537  icccncfext  46700  stoweidlem14  46827  stoweidlem34  46847  stoweidlem59  46872  etransclem24  47071  nnfoctbdjlem  47268  nnfoctbdj  47269  hspmbllem2  47440  nsssmfmbflem  47591  fsetsnprcnex  47928  eu2ndop1stv  47998  afvfv0bi  48025  afvco2  48049  ndmaovg  48057  ndfatafv2nrn  48094  afv2ndefb  48097  afv2fv0  48138  nelbr  48147  otiunsndisjX  48152  fun2dmnopgexmpl  48157  ltnltne  48172  readdcnnred  48176  resubcnnred  48177  recnmulnred  48178  cndivrenred  48179  ichnreuop  48357  nprmmul1  48412  fmtnoinf  48424  odz2prm2pw  48451  prmdvdsfmtnof1lem2  48473  lighneallem3  48495  lighneallem4  48498  requad1  48523  isodd3  48553  bits0ALTV  48580  nfermltl8rev  48643  nfermltl2rev  48644  nfermltlrev  48645  upgrimpths  48810  isubgr3stgrlem3  48869  usgrexmpl12ngric  48939  pgnbgreunbgrlem2lem1  49015  pgnbgreunbgrlem2lem2  49016  pgnbgreunbgrlem2lem3  49017  pgnbgreunbgrlem5lem1  49021  pgnbgreunbgrlem5lem2  49022  pgnbgreunbgrlem5lem3  49023  lgricngricex  49030  lidldomnnring  49136  smprngprmrng  49239  ztprmneprm  49262  lindepsnlininds  49367  islindeps  49368  lindslinindsimp2lem5  49377  lindslinindsimp2  49378  line2ylem  49666  line2xlem  49668  map0cor  49768  nelsubc3lem  49981  fulltermc2  50423  setc1onsubc  50513  cnelsubclem  50514  elsetrecslem  50610