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  845  con3ALT  1097  xorbi12d  1547  equsexvw  2027  cbvexvw  2059  cbvexdvaw  2061  excomimw  2066  hbe1w  2072  19.8aw  2074  exexw  2075  ru0  2163  cbvexv1  2375  cbvex2v  2377  drex1v  2403  cbvex  2432  cbvex2  2445  drex1  2474  eujustALT  2601  necon3abid  2995  neleq12d  3068  cbvrexdva  3245  cbvrexfw  3305  cbvrexdva2  3341  cbvrexf  3350  cbvexeqsetf  3471  ceqsex  3503  ceqsexv  3504  gencbval  3514  spcegf  3553  spc2gv  3561  spc2d  3563  spc3gv  3565  ceqsralbv  3618  cdeqnot  3733  rru  3744  sbcng  3793  sbcrext  3828  cbvrexcsf  3897  difjust  3908  eldif  3916  dfpss3  4044  dfdif3OLD  4074  difeq2  4076  disjne  4411  pssdifcom1  4445  eldifpr  4619  rexsng  4637  elpwunsn  4645  eldiftp  4648  rexprg  4658  preqsnd  4819  disjxun  5100  exnelv  5265  nalsetOLD  5267  dtruALT2  5329  dtruALT  5347  rexxfrd  5368  rexxfr2d  5370  rexxfrd2  5372  rexxfr  5375  opthneg  5451  snopeqop  5477  otiunsndisj  5491  poeq1  5560  pocl  5565  swopo  5568  sotric  5587  sotrieq  5588  isso2i  5594  somo  5596  freq1  5616  frirr  5625  fr2nr  5626  frminex  5628  tz7.2  5632  wereu2  5646  poinxp  5730  frinxp  5732  posn  5735  frsn  5737  rexiunxp  5814  rexxpf  5821  intirr  6107  poirr2  6113  cnvpo  6276  dfpo2  6285  predpoirr  6322  predfrirr  6323  frpomin  6329  nordeq  6367  ordtri1  6381  ordtri3  6384  fvmpti  6976  fndmdif  7025  rexrnmptw  7078  rexrnmpt  7080  rexima  7224  f1imapss  7252  f1ounsn  7258  cbvexfo  7276  nf1const  7290  soisoi  7314  isopolem  7331  weniso  7340  imaeqsalvOLD  7350  canth  7352  riotaclb  7396  rexrnmpo  7538  ndmovg  7581  sorpssuni  7717  sorpssint  7718  fr3nr  7757  dfwe2  7759  ordsucsssuc  7805  nlimsucg  7824  orduninsuc  7825  dfom2  7850  ssnlim  7868  resf1extb  7917  f1oweALT  7955  frxp  8108  poxp  8110  frxp2  8126  frxp3  8133  xpord3inddlem  8136  soseq  8141  suppofssd  8185  suppcoss  8189  smoword  8339  tz7.48lem  8414  oacan  8519  oaword  8520  omlimcl  8549  omeulem1  8553  nnaword  8599  nnmword  8605  nneob  8628  naddss1  8662  brdifun  8711  swoer  8712  undifixp  8918  boxcutc  8925  2dom  9013  php  9177  phpeqd  9182  nndomog  9183  onomeneq  9184  nnsdomo  9189  unxpdomlem2  9203  frfi  9231  unfilem1  9251  tfsnfin2  9308  supeq3  9397  supeq123d  9398  supmo  9400  eqsup  9404  supub  9407  sup0  9415  suppr  9420  supisolem  9422  supisoex  9423  eqinf  9433  infval  9435  infmo  9445  infpr  9453  infempty  9457  oieq1  9462  ordtypecbv  9467  ordtypelem7  9474  wemapsolem  9500  canthwdom  9529  zfregcl  9544  zfregclOLD  9545  elirrv  9547  elirrvOLD  9548  elirrvOLDOLD  9549  elirr  9550  noinfep  9617  cantnfp1lem3  9637  ttrcltr  9673  rankr1clem  9780  carden2b  9927  domtri2  9949  alephord3  10036  alephdom2  10045  alephval3  10068  dfac9  10095  kmlem2  10110  kmlem4  10112  isfin4  10256  isfin7  10260  fin23lem11  10276  isf32lem5  10316  isf34lem4  10336  fin1a2lem6  10364  fin1a2lem7  10365  fin1a2lem12  10370  itunisuc  10378  ac6n  10444  zorn2g  10462  zornn0g  10464  ttukeylem7  10474  infinfg  10525  axpowndlem3  10559  axpowndlem4  10560  axregnd  10564  elgch  10582  engch  10588  fpwwe2lem12  10602  fpwwe2  10603  pwfseqlem1  10618  pwfseqlem3  10620  hargch  10633  addnidpi  10861  pinq  10887  nqereu  10889  ltsonq  10929  prlem934  10993  ltexprlem7  11002  addcanpr  11006  prlem936  11007  reclem2pr  11008  reclem3pr  11009  supexpr  11014  ltsosr  11054  supsrlem  11071  axpre-lttri  11125  axpre-sup  11129  xrlenlt  11249  axlttri  11256  axsup  11260  ltne  11282  dedekind  11348  readdcan  11359  leadd1  11657  ltsub1  11685  ltsub2  11686  leord1  11716  lediv1  12059  lemuldiv  12074  lerec  12077  le2msq  12094  infm3  12153  suprnub  12159  infregelb  12178  avgle1  12463  avgle2  12464  znnnlt1  12600  indstr  12919  zsupss  12940  uzsupss  12943  rpneg  13029  xralrple  13210  xleneg  13223  xltadd1  13261  xposdif  13267  xmulneg1  13274  xltmul1  13297  xrsupexmnf  13310  xrinfmexpnf  13311  xrsupsslem  13312  xrinfmsslem  13313  xrub  13317  supxrleub  13331  infxrgelb  13341  difreicc  13490  nn0disj  13651  nelfzo  13672  elfznelfzo  13781  fvinim0ffz  13797  injresinjlem  13798  ssnn0fi  14000  leexp2  14186  exp11nnd  14276  hashbnd  14351  hasheni  14363  hashfundm  14457  hashbc  14468  wrdsymb0  14564  swrdnd  14670  swrdnd2  14671  pfxnd0  14704  repswswrd  14799  repswccat  14801  cshwidxmod  14818  cnpart  15269  sqrtlt  15290  limsuplt  15508  rlimrege0  15608  isercoll  15697  efle  16152  odd2np1  16377  sumodd  16424  divalglem7  16435  ndvdsadd  16446  fldivndvdslt  16452  bitsfval  16459  bitsval  16460  bits0  16464  bitsp1  16467  bitsmod  16472  bitscmp  16474  bitsinv1lem  16477  sadadd2lem2  16486  saddisjlem  16500  bitsshft  16511  gcdneg  16558  algcvgblem  16613  lcmneg  16639  isprm3  16719  dvdsnprmd  16726  isprm5  16744  rpexp  16759  phiprmpw  16813  m1dvdsndvds  16836  pythagtrip  16872  pcgcd1  16915  prmpwdvds  16942  prmreclem2  16955  prmreclem3  16956  prmreclem5  16958  prmreclem6  16959  vdwlem6  17024  vdwnnlem2  17034  vdwnnlem3  17035  vdwnn  17036  prmlem0  17143  prmlem1a  17144  divsfval  17579  mrisval  17664  ismri  17665  ismri2dad  17671  cidpropd  17744  cat1lem  18131  plttr  18374  joinval  18409  meetval  18423  acsfiindd  18587  isnsgrp  18759  smndex1n0mnd  18951  mgm2nsgrplem2  18958  sgrp2nmndlem3  18964  symgpssefmnd  19438  symgfix2  19458  pmtrdifellem4  19521  psgnunilem1  19535  psgnunilem5  19536  psgnunilem2  19537  psgnunilem3  19538  pmtrsn  19561  sylow1lem3  19642  sylow2alem2  19660  efgsfo  19781  ablfac1eulem  20116  ablfac1eu  20117  pgpfac1lem1  20118  pgpfac1lem5  20123  nzrunit  20576  zrninitoringc  20728  islbs  21145  lbsind  21149  lbspss  21151  lbspropd  21168  lspsnne1  21189  islbs2  21226  lbsacsbs  21228  lbsextlem1  21230  lbsextlem3  21232  lbsextlem4  21233  lbsextg  21234  frlmlbs  21851  islindf  21866  islinds2  21867  islindf2  21868  lindfind  21870  lindsind  21871  lindfrn  21875  lindfmm  21881  lsslindf  21884  islindf4  21892  opsrtoslem2  22111  psdmul  22233  cply1coe0  22366  cply1coe0bi  22367  mdetunilem7  22680  mdetunilem8  22681  mdetunilem9  22682  maducoeval2  22702  pmatcollpw3fi1lem1  22848  fvmptnn04ifa  22912  fvmptnn04ifc  22914  fvmptnn04ifd  22915  chfacffsupp  22918  chfacfscmul0  22920  chfacfpmmul0  22924  elcls  23135  maxlp  23209  perfi  23217  ordtbaslem  23250  ordtval  23251  ordtbas2  23253  ordtopn1  23256  ordtopn2  23257  ordtcnv  23263  ordtrest  23264  ordtrest2lem  23265  ordtrest2  23266  pnfnei  23282  mnfnei  23283  isreg2  23439  ordthauslem  23445  cmpfi  23470  cmpfii  23471  bwth  23472  nconnsubb  23485  hausdiag  23707  txkgen  23714  kqdisj  23794  ordthmeolem  23863  fbfinnfr  23903  trfbas  23906  fbunfip  23931  fbasrn  23946  trfil3  23950  ufileu  23981  fin1aufil  23994  hausflim  24043  alexsubALTlem2  24110  alexsubALTlem3  24111  alexsubALTlem4  24112  ptcmplem2  24115  ptcmplem3  24116  stdbdbl  24579  iccntr  24884  reconnlem2  24890  iccpnfcnv  25008  xrhmeo  25010  lebnumlem1  25025  lebnumlem2  25026  lebnumlem3  25027  bcthlem4  25391  minveclem3b  25492  ivthlem2  25516  ivthlem3  25517  mbfmax  25713  mbfposr  25716  i1fd  25745  mbfi1fseqlem4  25782  itg2splitlem  25812  itg2monolem1  25814  itg2cnlem1  25825  dvne0  26075  lhop1lem  26077  deg1nn0clb  26152  dgrle  26305  coemulhi  26316  plymulidp  26348  aaliou3lem9  26416  cos11  26600  logleb  26670  argrege0  26678  logdivle  26689  ellogdm  26706  cxple  26762  cxplt2  26765  cxple3  26768  isosctrlem1  26885  atandm  26943  atans2  26998  atantayl2  27005  eldmgm  27088  ftalem7  27145  isppw2  27181  musum  27257  dchrsum2  27334  bposlem1  27350  lgsmod  27389  lgsdir2lem2  27392  lgsdir2  27396  lgsne0  27401  lgsprme0  27405  gausslemma2dlem4  27435  lgsquadlem1  27446  2lgslem3  27470  2lgsoddprm  27482  2sq2  27499  addsqrexnreu  27508  rpvmasumlem  27553  padicabv  27696  ostth3  27704  ostth  27705  noextenddif  27734  nodenselem4  27753  nodenselem5  27754  nodenselem7  27756  nolt02o  27761  nogt01o  27762  noresle  27763  nosupprefixmo  27766  noinfprefixmo  27767  nosupcbv  27768  nosupdm  27770  nosupfv  27772  nosupres  27773  nosupbnd1lem1  27774  nosupbnd1lem3  27776  nosupbnd1lem5  27778  nosupbnd1  27780  nosupbnd2lem1  27781  nosupbnd2  27782  noinfcbv  27783  noinfdm  27785  noinffv  27787  noinfres  27788  noinfbnd1lem1  27789  noinfbnd1lem3  27791  noinfbnd1lem5  27793  noinfbnd1  27795  noinfbnd2lem1  27796  noinfbnd2  27797  lenlts  27818  ltsne  27840  nocvxminlem  27849  lesrec  27894  eqcuts3  27899  cuteq1  27912  newbday  27997  ltslpss  28003  cofcutr  28019  lrrecfr  28038  addsval  28057  ltadds2  28086  lenegs  28141  lesubsubsbd  28181  lesubsubs2bd  28182  lesubsubs3bd  28183  lesubaddsd  28188  ltmuls2  28266  lemuls2d  28269  lemuls1d  28270  oncutlt  28359  onles  28363  pw2cut2  28557  bdaypw2bnd  28560  bdayfinbndlem1  28562  istrkgld  28630  axtgupdim2  28642  tglowdim2l  28822  axlowdimlem16  29160  axlowdim2  29163  axlowdim  29164  numedglnl  29347  usgredg2v  29430  lfuhgr1v0e  29457  cusgrfi  29661  vtxd0nedgb  29691  vtxduhgr0edgnel  29697  1loopgrnb0  29705  1hevtxdg0  29708  vtxdgoddnumeven  29756  wlkp1lem1  29874  wlkp1lem2  29875  wlkp1lem5  29878  dfpth2  29931  crctcsh  30026  clwlkclwwlklem2a4  30201  eupth2eucrct  30421  eupth2lem3lem3  30434  eupth2lem3lem4  30435  eupth2lem3lem6  30437  eupth2lem3lem7  30438  eupth2lems  30442  eupth2  30443  konigsberglem4  30459  nfrgr2v  30476  frgrwopreglem3  30518  fusgr2wsp2nb  30538  frgrreggt1  30597  friendshipgt3  30602  lpni  30685  nmobndseqi  30984  minvecolem5  31086  chpsscon3  31708  chnle  31719  nonbooli  31856  pjnel  31931  specval  32103  nmcfnlbi  32257  stri  32462  hstri  32470  cvbr  32487  cvcon3  32489  chcv1  32560  cvexchlem  32573  chrelat2  32575  nelun  32714  elpreq  32729  nelpr  32732  ifeqeqx  32743  nfpconfp  32836  suppiniseg  32890  isoun  32906  suppss3  32927  xrge0infss  32964  infxrge0gelb  32970  eliccelico  32981  elicoelioo  32982  nndiffz1  32990  hashgt1  33012  expgt0b  33021  nn0min  33025  ccatws1f1o  33131  toslublem  33152  tosglblem  33154  pmtrcnel  33271  cycpmco2  33315  isarchi2  33367  archiabl  33380  elrgspnlem2  33426  elrgspnlem3  33427  0nellinds  33558  lindssn  33566  lindfpropd  33570  ssdifidlprm  33647  mxidlirred  33662  ssmxidl  33664  dflringlem  33692  esplyind  33874  lbslsat  33915  lindsunlem  33923  rtelextdg2lem  34025  constrsqrtcl  34078  ordtcnvNEW  34219  ordtrestNEW  34220  ordtrest2NEWlem  34221  ordtrest2NEW  34222  ordtconnlem1  34223  xrge0iifcnv  34232  esumpcvgval  34377  esum2d  34392  ddemeas  34535  omssubadd  34599  oddpwdc  34653  eulerpartlems  34659  eulerpartlemf  34669  eulerpartlemt  34670  eulerpartlemr  34673  eulerpartlemgvv  34675  eulerpartlemn  34680  ballotlemfc0  34792  ballotlemfcc  34793  ballotlem4  34798  ballotlemimin  34805  ballotlem7  34835  signsply0  34847  reprinfz1  34918  reprpmtf1o  34922  reprdifc  34923  hgt750lema  34953  hgt750leme  34954  istrkg2d  34962  bnj23  35016  bnj1185  35090  bnj1228  35308  bnj1388  35330  bnj1417  35338  ordtypeon  35388  nummin  35391  axprALT2  35409  fineqvnttrclselem1  35421  axnulg  35445  onvf1odlem2  35451  onvf1odlem3  35452  revwlk  35480  isacycgr  35500  acycgr0v  35503  prclisacycgr  35506  erdszelem10  35555  satf0n0  35733  fmlaomn0  35745  fmlasucdisj  35754  satfv1fvfmla1  35778  satefvfmla1  35780  ismfs  35904  mvtinf  35910  untelirr  36063  untsucf  36065  untangtr  36069  dfon2lem3  36138  dfon2lem4  36139  dfon2lem7  36142  dfon2lem9  36144  distel  36156  funpartfv  36300  dfrdg4  36306  nmulprop  36545  nn0prpwlem  36687  nn0prpw  36688  limsucncmpi  36810  limsucncmp  36811  ordcmp  36812  weiunlem  36828  weiunfrlem  36829  weiunfr  36832  axtcond  36843  regsfromregtco  36903  regsfromsetind  36904  unblimceq0  36950  unbdqndv1  36951  bj-hbntbi  37184  bj-equsexvwd  37253  bj-cbvexdv  37290  bj-ru1  37433  bj-nuliota  37547  topdifinffinlem  37846  topdifinffin  37847  icorempo  37850  relowlpssretop  37863  finxpreclem2  37889  finxpreclem6  37895  wl-issetft  38090  wl-eujustlem1  38096  leceifl  38113  lindsadd  38117  lindsenlbs  38119  matunitlindflem1  38120  poimirlem16  38140  poimirlem17  38141  poimirlem18  38142  poimirlem19  38143  poimirlem21  38145  poimirlem23  38147  poimirlem26  38150  poimirlem27  38151  poimirlem28  38152  poimirlem31  38155  poimir  38157  mblfinlem2  38162  mblfinlem3  38163  ismblfin  38165  cnambfre  38172  itg2addnclem  38175  itg2addnclem2  38176  iblabsnclem  38187  ftc1anclem1  38197  areacirc  38217  heibor1lem  38313  heiborlem1  38315  heiborlem6  38320  heiborlem8  38322  heiborlem10  38324  smprngopr  38556  ecin0  38856  ax12inda  39577  riotaclbgBAD  39583  lcvfbr  39649  lcvbr  39650  lsatcv0  39660  l1cvpat  39683  opltcon3b  39833  cvrfval  39897  cvrval  39898  cvrnbtwn  39900  cvrval2  39903  cvrnbtwn2  39904  cvrnbtwn3  39905  cvrcon3b  39906  cvrnbtwn4  39908  atnlt  39942  iscvlat  39952  cvlexch1  39957  hlsuprexch  40010  hlrelat5N  40030  hlrelat2  40032  cvrval5  40044  3dimlem1  40087  3dim1lem5  40095  3dim2  40097  3dim3  40098  llnnlt  40152  islpln5  40164  lplni2  40166  lvolex3N  40167  lplnnle2at  40170  islpln2a  40177  lplnribN  40180  lplnexllnN  40193  lplnnlt  40194  lvoli3  40206  islvol5  40208  lvoli2  40210  lvolnle3at  40211  islvol2aN  40221  4atlem11  40238  lvolnltN  40247  dalawlem15  40514  4atexlemex2  40700  4atex  40705  4atex2-0aOLDN  40707  4atex2-0cOLDN  40709  lautcvr  40721  ltrnfset  40746  ltrnset  40747  ltrnu  40750  trlfset  40789  trlset  40790  trlval2  40792  cdlemd6  40832  cdleme0nex  40919  cdleme18d  40924  cdleme25b  40983  cdleme25cv  40987  cdleme29b  41004  cdleme31fv  41019  cdleme31fv2  41022  cdlemefrs29bpre0  41025  cdlemefr32sn2aw  41033  cdlemefr29bpre0N  41035  cdlemefr29clN  41036  cdlemefr32fvaN  41038  cdlemefr32fva1  41039  cdlemefs32sn1aw  41043  cdleme32fva  41066  cdleme32fvaw  41068  cdleme40v  41098  cdleme42b  41107  cdleme46f2g2  41122  cdleme46f2g1  41123  cdleme48gfv  41166  cdlemg1fvawlemN  41202  cdlemg1cex  41217  cdlemg6d  41250  cdlemm10N  41747  dicffval  41803  dicfval  41804  dicval  41805  dicfnN  41812  dicvalrelN  41814  dihffval  41859  dihfval  41860  dihlsscpre  41863  dvh4dimat  42067  dvh3dimatN  42068  dvh4dimlem  42072  dvh3dim  42075  dvh4dimN  42076  dvh3dim2  42077  dvh3dim3N  42078  mapdcv  42289  mapdh9aOLDN  42419  hdmapfval  42456  hdmapval  42457  hdmapval2  42461  hdmap11lem2  42471  dvrelog2b  42688  aks4d1p4  42701  aks4d1p5  42702  aks4d1p7  42705  aks4d1p8d2  42707  aks4d1p8  42709  aks4d1  42711  aks6d1c2p2  42741  hashnexinj  42750  rspcsbnea  42753  aks6d1c5  42761  aks6d1c6lem3  42794  aks6d1c7  42806  supinf  42863  oexpreposd  42936  mullt0b2d  43111  flt4lem7  43246  nna4b4nsq  43247  ellz1  43353  rencldnfilem  43402  jm2.22  43577  jm2.23  43578  wepwsolem  43624  fnwe2lem2  43633  aomclem8  43643  unxpwdom3  43677  onsupmaxb  43821  onexlimgt  43825  onsupeqnmax  43829  onov0suclim  43856  oaordnr  43878  omnord1  43887  oenord1  43898  oaomoencom  43899  oenass  43901  cantnfresb  43906  tfsnfin  43934  ralopabb  43992  nlimsuc  44022  ifpbi12  44069  dfsucon  44104  sqrtcvallem1  44212  ss2iundf  44240  frege124d  44342  clsk3nimkb  44621  clsk1indlem1  44626  clsk1independent  44627  ntrneineine1lem  44665  ntrneicls11  44671  clsneiel1  44689  clsneiel2  44690  neicvgel1  44700  neicvgel2  44701  radcnvrat  44895  rusbcALT  45019  en3lpVD  45425  0elaxnul  45564  omssaxinf2  45569  permaxnul  45589  permaxinf2lem  45593  nregmodel  45598  eliin2f  45687  nssd  45688  wessf1ornlem  45768  rexanuz2nf  46071  limsupre2lem  46303  icccncfext  46466  stoweidlem14  46593  stoweidlem34  46613  stoweidlem59  46638  etransclem24  46837  nnfoctbdjlem  47034  nnfoctbdj  47035  hspmbllem2  47206  nsssmfmbflem  47357  fsetsnprcnex  47654  eu2ndop1stv  47724  afvfv0bi  47751  afvco2  47775  ndmaovg  47783  ndfatafv2nrn  47820  afv2ndefb  47823  afv2fv0  47864  nelbr  47873  otiunsndisjX  47878  fun2dmnopgexmpl  47883  ltnltne  47898  readdcnnred  47902  resubcnnred  47903  recnmulnred  47904  cndivrenred  47905  ichnreuop  48083  nprmmul1  48138  fmtnoinf  48150  odz2prm2pw  48177  prmdvdsfmtnof1lem2  48199  lighneallem3  48221  lighneallem4  48224  requad1  48249  isodd3  48279  bits0ALTV  48306  nfermltl8rev  48369  nfermltl2rev  48370  nfermltlrev  48371  upgrimpths  48536  isubgr3stgrlem3  48595  usgrexmpl12ngric  48665  pgnbgreunbgrlem2lem1  48741  pgnbgreunbgrlem2lem2  48742  pgnbgreunbgrlem2lem3  48743  pgnbgreunbgrlem5lem1  48747  pgnbgreunbgrlem5lem2  48748  pgnbgreunbgrlem5lem3  48749  lgricngricex  48756  lidldomnnring  48863  ztprmneprm  48974  lindepsnlininds  49079  islindeps  49080  lindslinindsimp2lem5  49089  lindslinindsimp2  49090  line2ylem  49378  line2xlem  49380  map0cor  49481  nelsubc3lem  49696  fulltermc2  50138  setc1onsubc  50228  cnelsubclem  50229  elsetrecslem  50325