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 ⊢ (𝜑 → (¬ 𝜓 ↔ ¬ 𝜒))

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

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 210

This theorem is referenced by:  notbi  322  annotanannot  847  con3ALT  1099  xorbi12d  1553  equsexvw  2033  cbvexvw  2065  cbvexdvaw  2067  excomimw  2072  hbe1w  2078  19.8aw  2080  exexw  2081  ru0  2160  cbvexv1  2372  cbvex2v  2374  drex1v  2400  cbvex  2429  cbvex2  2442  drex1  2471  eujustALT  2598  necon3abid  2992  neleq12d  3067  cbvrexdva  3244  cbvrexfw  3304  cbvrexdva2  3339  cbvrexf  3348  cbvexeqsetf  3468  ceqsex  3500  ceqsexv  3501  gencbval  3511  spcegf  3550  spc2gv  3558  spc2d  3560  spc3gv  3562  ceqsralbv  3615  cdeqnot  3730  rru  3741  sbcng  3790  sbcrext  3825  cbvrexcsf  3895  difjust  3906  eldif  3914  dfpss3  4042  dfdif3OLD  4072  difeq2  4074  disjne  4414  pssdifcom1  4449  eldifpr  4623  rexsng  4641  elpwunsn  4649  eldiftp  4652  rexprg  4662  preqsnd  4823  disjxun  5106  exnelv  5275  nalsetOLD  5277  dtruALT2  5341  dtruALT  5359  rexxfrd  5380  rexxfr2d  5382  rexxfrd2  5384  rexxfr  5387  opthneg  5463  snopeqop  5489  otiunsndisj  5503  poeq1  5572  pocl  5577  swopo  5580  sotric  5599  sotrieq  5600  isso2i  5606  somo  5608  freq1  5628  frirr  5637  fr2nr  5638  frminex  5640  tz7.2  5644  wereu2  5658  poinxp  5742  frinxp  5744  posn  5747  frsn  5749  rexiunxp  5826  rexxpf  5833  intirr  6118  poirr2  6124  cnvpo  6288  dfpo2  6297  predpoirr  6334  predfrirr  6335  frpomin  6341  nordeq  6379  ordtri1  6394  ordtri3  6397  fvmpti  6988  fndmdif  7037  rexrnmptw  7090  rexrnmpt  7092  rexima  7236  f1imapss  7264  f1ounsn  7270  cbvexfo  7288  nf1const  7302  soisoi  7326  isopolem  7343  weniso  7352  imaeqsalvOLD  7362  canth  7364  riotaclb  7408  rexrnmpo  7550  ndmovg  7593  sorpssuni  7729  sorpssint  7730  fr3nr  7770  dfwe2  7772  ordsucsssuc  7818  nlimsucg  7837  orduninsuc  7838  dfom2  7863  ssnlim  7881  resf1extb  7930  f1oweALT  7968  frxp  8121  poxp  8123  frxp2  8139  frxp3  8146  xpord3inddlem  8149  soseq  8154  suppofssd  8198  suppcoss  8202  smoword  8352  tz7.48lem  8427  oacan  8532  oaword  8533  omlimcl  8562  omeulem1  8566  nnaword  8612  nnmword  8618  nneob  8641  naddss1  8675  brdifun  8724  swoer  8725  undifixp  8931  boxcutc  8938  2dom  9026  php  9190  phpeqd  9195  nndomog  9196  onomeneq  9197  nnsdomo  9202  unxpdomlem2  9216  frfi  9244  unfilem1  9264  tfsnfin2  9319  supeq3  9408  supeq123d  9409  supmo  9411  eqsup  9415  supub  9418  sup0  9426  suppr  9431  supisolem  9433  supisoex  9434  eqinf  9444  infval  9446  infmo  9456  infpr  9464  infempty  9468  oieq1  9473  ordtypecbv  9478  ordtypelem7  9485  wemapsolem  9511  canthwdom  9540  zfregcl  9555  zfregclOLD  9556  elirrv  9558  elirrvOLD  9559  elirrvOLDOLD  9560  elirr  9561  noinfep  9628  cantnfp1lem3  9648  ttrcltr  9684  rankr1clem  9791  carden2b  9952  domtri2  9974  alephord3  10061  alephdom2  10070  alephval3  10093  dfac9  10119  kmlem2  10134  kmlem4  10136  isfin4  10280  isfin7  10284  fin23lem11  10300  isf32lem5  10340  isf34lem4  10360  fin1a2lem6  10388  fin1a2lem7  10389  fin1a2lem12  10394  itunisuc  10402  ac6n  10468  zorn2g  10486  zornn0g  10488  ttukeylem7  10498  infinfg  10549  axpowndlem3  10583  axpowndlem4  10584  axregnd  10588  elgch  10606  engch  10612  fpwwe2lem12  10626  fpwwe2  10627  pwfseqlem1  10642  pwfseqlem3  10644  hargch  10657  addnidpi  10885  pinq  10911  nqereu  10913  ltsonq  10953  prlem934  11017  ltexprlem7  11026  addcanpr  11030  prlem936  11031  reclem2pr  11032  reclem3pr  11033  supexpr  11038  ltsosr  11078  supsrlem  11095  axpre-lttri  11149  axpre-sup  11153  xrlenlt  11273  axlttri  11280  axsup  11284  ltne  11306  dedekind  11372  readdcan  11383  leadd1  11681  ltsub1  11709  ltsub2  11710  leord1  11740  lediv1  12079  lemuldiv  12094  lerec  12097  le2msq  12114  infm3  12173  suprnub  12179  infregelb  12198  avgle1  12483  avgle2  12484  znnnlt1  12620  indstr  12939  zsupss  12960  uzsupss  12963  rpneg  13049  xralrple  13230  xleneg  13243  xltadd1  13281  xposdif  13287  xmulneg1  13294  xltmul1  13317  xrsupexmnf  13330  xrinfmexpnf  13331  xrsupsslem  13332  xrinfmsslem  13333  xrub  13337  supxrleub  13351  infxrgelb  13361  difreicc  13510  nn0disj  13671  nelfzo  13692  elfznelfzo  13801  fvinim0ffz  13817  injresinjlem  13818  ssnn0fi  14020  leexp2  14206  exp11nnd  14296  hashbnd  14371  hasheni  14383  hashfundm  14478  hashbc  14489  wrdsymb0  14585  swrdnd  14691  swrdnd2  14692  pfxnd0  14725  repswswrd  14820  repswccat  14822  cshwidxmod  14839  cnpart  15290  sqrtlt  15311  limsuplt  15529  rlimrege0  15629  isercoll  15718  efle  16173  odd2np1  16398  sumodd  16445  divalglem7  16456  ndvdsadd  16467  fldivndvdslt  16473  bitsfval  16480  bitsval  16481  bits0  16485  bitsp1  16488  bitsmod  16493  bitscmp  16495  bitsinv1lem  16498  sadadd2lem2  16507  saddisjlem  16521  bitsshft  16532  gcdneg  16579  algcvgblem  16634  lcmneg  16660  isprm3  16740  dvdsnprmd  16747  isprm5  16765  rpexp  16780  phiprmpw  16834  m1dvdsndvds  16857  pythagtrip  16893  pcgcd1  16936  prmpwdvds  16963  prmreclem2  16976  prmreclem3  16977  prmreclem5  16979  prmreclem6  16980  vdwlem6  17045  vdwnnlem2  17055  vdwnnlem3  17056  vdwnn  17057  prmlem0  17164  prmlem1a  17165  divsfval  17600  mrisval  17685  ismri  17686  ismri2dad  17692  cidpropd  17765  cat1lem  18152  plttr  18395  joinval  18430  meetval  18444  acsfiindd  18608  isnsgrp  18780  smndex1n0mnd  18973  mgm2nsgrplem2  18980  sgrp2nmndlem3  18986  symgpssefmnd  19465  symgfix2  19485  pmtrdifellem4  19548  psgnunilem1  19562  psgnunilem5  19563  psgnunilem2  19564  psgnunilem3  19565  pmtrsn  19588  sylow1lem3  19669  sylow2alem2  19687  efgsfo  19808  ablfac1eulem  20143  ablfac1eu  20144  pgpfac1lem1  20145  pgpfac1lem5  20150  nzrunit  20607  zrninitoringc  20760  islbs  21176  lbsind  21180  lbspss  21182  lbspropd  21199  lspsnne1  21220  islbs2  21257  lbsacsbs  21259  lbsextlem1  21261  lbsextlem3  21263  lbsextlem4  21264  lbsextg  21265  ssdifidlprm  21465  frlmlbs  21926  islindf  21941  islinds2  21942  islindf2  21943  lindfind  21945  lindsind  21946  lindfrn  21950  lindfmm  21956  lsslindf  21959  islindf4  21967  opsrtoslem2  22186  psdmul  22308  cply1coe0  22440  cply1coe0bi  22441  mdetunilem7  22754  mdetunilem8  22755  mdetunilem9  22756  maducoeval2  22776  pmatcollpw3fi1lem1  22922  fvmptnn04ifa  22986  fvmptnn04ifc  22988  fvmptnn04ifd  22989  chfacffsupp  22992  chfacfscmul0  22994  chfacfpmmul0  22998  elcls  23209  maxlp  23283  perfi  23291  ordtbaslem  23324  ordtval  23325  ordtbas2  23327  ordtopn1  23330  ordtopn2  23331  ordtcnv  23337  ordtrest  23338  ordtrest2lem  23339  ordtrest2  23340  pnfnei  23356  mnfnei  23357  isreg2  23513  ordthauslem  23519  cmpfi  23544  cmpfii  23545  bwth  23546  nconnsubb  23559  hausdiag  23781  txkgen  23788  kqdisj  23868  ordthmeolem  23937  fbfinnfr  23977  trfbas  23980  fbunfip  24005  fbasrn  24020  trfil3  24024  ufileu  24055  fin1aufil  24068  hausflim  24117  alexsubALTlem2  24184  alexsubALTlem3  24185  alexsubALTlem4  24186  ptcmplem2  24189  ptcmplem3  24190  stdbdbl  24653  iccntr  24958  reconnlem2  24964  iccpnfcnv  25082  xrhmeo  25084  lebnumlem1  25099  lebnumlem2  25100  lebnumlem3  25101  bcthlem4  25465  minveclem3b  25566  ivthlem2  25590  ivthlem3  25591  mbfmax  25787  mbfposr  25790  i1fd  25819  mbfi1fseqlem4  25856  itg2splitlem  25886  itg2monolem1  25888  itg2cnlem1  25899  dvne0  26149  lhop1lem  26151  deg1nn0clb  26226  dgrle  26379  coemulhi  26390  plymulidp  26422  aaliou3lem9  26490  cos11  26674  logleb  26744  argrege0  26752  logdivle  26763  ellogdm  26780  cxple  26836  cxplt2  26839  cxple3  26842  isosctrlem1  26959  atandm  27017  atans2  27072  atantayl2  27079  eldmgm  27162  ftalem7  27219  isppw2  27255  musum  27331  dchrsum2  27408  bposlem1  27424  lgsmod  27463  lgsdir2lem2  27466  lgsdir2  27470  lgsne0  27475  lgsprme0  27479  gausslemma2dlem4  27509  lgsquadlem1  27520  2lgslem3  27544  2lgsoddprm  27556  2sq2  27573  addsqrexnreu  27582  rpvmasumlem  27627  padicabv  27770  ostth3  27778  ostth  27779  noextenddif  27808  nodenselem4  27827  nodenselem5  27828  nodenselem7  27830  nolt02o  27835  nogt01o  27836  noresle  27837  nosupprefixmo  27840  noinfprefixmo  27841  nosupcbv  27842  nosupdm  27844  nosupfv  27846  nosupres  27847  nosupbnd1lem1  27848  nosupbnd1lem3  27850  nosupbnd1lem5  27852  nosupbnd1  27854  nosupbnd2lem1  27855  nosupbnd2  27856  noinfcbv  27857  noinfdm  27859  noinffv  27861  noinfres  27862  noinfbnd1lem1  27863  noinfbnd1lem3  27865  noinfbnd1lem5  27867  noinfbnd1  27869  noinfbnd2lem1  27870  noinfbnd2  27871  lenlts  27892  ltsne  27914  nocvxminlem  27923  lesrec  27968  eqcuts3  27973  cuteq1  27986  newbday  28071  ltslpss  28077  cofcutr  28093  lrrecfr  28112  addsval  28131  ltadds2  28160  lenegs  28215  lesubsubsbd  28255  lesubsubs2bd  28256  lesubsubs3bd  28257  lesubaddsd  28262  ltmuls2  28340  lemuls2d  28343  lemuls1d  28344  oncutlt  28433  onles  28437  pw2cut2  28631  bdaypw2bnd  28634  bdayfinbndlem1  28636  istrkgld  28704  axtgupdim2  28716  tglowdim2l  28900  axlowdimlem16  29273  axlowdim2  29276  axlowdim  29277  numedglnl  29460  usgredg2v  29543  lfuhgr1v0e  29570  cusgrfi  29774  vtxd0nedgb  29804  vtxduhgr0edgnel  29810  1loopgrnb0  29818  1hevtxdg0  29821  vtxdgoddnumeven  29869  wlkp1lem1  29987  wlkp1lem2  29988  wlkp1lem5  29991  dfpth2  30044  crctcsh  30139  clwlkclwwlklem2a4  30314  eupth2eucrct  30534  eupth2lem3lem3  30547  eupth2lem3lem4  30548  eupth2lem3lem6  30550  eupth2lem3lem7  30551  eupth2lems  30555  eupth2  30556  konigsberglem4  30572  nfrgr2v  30589  frgrwopreglem3  30631  fusgr2wsp2nb  30651  frgrreggt1  30710  friendshipgt3  30715  lpni  30798  nmobndseqi  31097  minvecolem5  31199  chpsscon3  31821  chnle  31832  nonbooli  31969  pjnel  32044  specval  32216  nmcfnlbi  32370  stri  32575  hstri  32583  cvbr  32600  cvcon3  32602  chcv1  32673  cvexchlem  32686  chrelat2  32688  nelun  32825  elpreq  32840  nelpr  32843  ifeqeqx  32854  nfpconfp  32943  suppiniseg  32997  isoun  33013  suppss3  33034  xrge0infss  33071  infxrge0gelb  33077  eliccelico  33088  elicoelioo  33089  nndiffz1  33097  hashgt1  33119  expgt0b  33127  nn0min  33131  ccatws1f1o  33237  toslublem  33258  tosglblem  33260  pmtrcnel  33375  cycpmco2  33419  isarchi2  33471  archiabl  33484  elrgspnlem2  33529  elrgspnlem3  33530  0nellinds  33651  lindssn  33657  lindfpropd  33661  mxidlirred  33721  ssmxidl  33723  dflringlem  33750  esplyind  33931  lbslsat  33972  lindsunlem  33980  rtelextdg2lem  34082  constrsqrtcl  34135  ordtcnvNEW  34276  ordtrestNEW  34277  ordtrest2NEWlem  34278  ordtrest2NEW  34279  ordtconnlem1  34280  xrge0iifcnv  34289  esumpcvgval  34434  esum2d  34449  ddemeas  34592  omssubadd  34656  oddpwdc  34710  eulerpartlems  34716  eulerpartlemf  34726  eulerpartlemt  34727  eulerpartlemr  34730  eulerpartlemgvv  34732  eulerpartlemn  34737  ballotlemfc0  34849  ballotlemfcc  34850  ballotlem4  34855  ballotlemimin  34862  ballotlem7  34892  signsply0  34904  reprinfz1  34975  reprpmtf1o  34979  reprdifc  34980  hgt750lema  35010  hgt750leme  35011  istrkg2d  35019  bnj23  35073  bnj1185  35147  bnj1228  35365  bnj1388  35387  bnj1417  35395  ordtypeon  35445  nummin  35448  axprALT2  35467  fineqvnttrclselem1  35488  axnulg  35512  onvf1odlem2  35542  onvf1odlem3  35543  revwlk  35571  isacycgr  35591  acycgr0v  35594  prclisacycgr  35597  erdszelem10  35646  satf0n0  35824  fmlaomn0  35836  fmlasucdisj  35845  satfv1fvfmla1  35869  satefvfmla1  35871  ismfs  35995  mvtinf  36001  untelirr  36154  untsucf  36156  untangtr  36160  dfon2lem3  36229  dfon2lem4  36230  dfon2lem7  36233  dfon2lem9  36235  distel  36247  funpartfv  36391  dfrdg4  36397  nmulprop  36636  nn0prpwlem  36777  nn0prpw  36778  limsucncmpi  36900  limsucncmp  36901  ordcmp  36902  weiunlem  36918  weiunfrlem  36919  weiunfr  36922  axtcond  36933  regsfromregtco  36993  regsfromsetind  36994  unblimceq0  37040  unbdqndv1  37041  bj-hbntbi  37273  bj-equsexvwd  37342  bj-cbvexdv  37379  bj-ru1  37523  bj-nuliota  37637  topdifinffinlem  37937  topdifinffin  37938  icorempo  37941  relowlpssretop  37954  finxpreclem2  37980  finxpreclem6  37986  wl-issetft  38181  wl-eujustlem1  38187  leceifl  38204  lindsadd  38208  lindsenlbs  38210  matunitlindflem1  38211  poimirlem16  38231  poimirlem17  38232  poimirlem18  38233  poimirlem19  38234  poimirlem21  38236  poimirlem23  38238  poimirlem26  38241  poimirlem27  38242  poimirlem28  38243  poimirlem31  38246  poimir  38248  mblfinlem2  38253  mblfinlem3  38254  ismblfin  38256  cnambfre  38263  itg2addnclem  38266  itg2addnclem2  38267  iblabsnclem  38278  ftc1anclem1  38288  areacirc  38308  heibor1lem  38404  heiborlem1  38406  heiborlem6  38411  heiborlem8  38413  heiborlem10  38415  smprngopr  38647  ecin0  38947  ax12inda  39668  riotaclbgBAD  39674  lcvfbr  39740  lcvbr  39741  lsatcv0  39751  l1cvpat  39774  opltcon3b  39924  cvrfval  39988  cvrval  39989  cvrnbtwn  39991  cvrval2  39994  cvrnbtwn2  39995  cvrnbtwn3  39996  cvrcon3b  39997  cvrnbtwn4  39999  atnlt  40033  iscvlat  40043  cvlexch1  40048  hlsuprexch  40101  hlrelat5N  40121  hlrelat2  40123  cvrval5  40135  3dimlem1  40178  3dim1lem5  40186  3dim2  40188  3dim3  40189  llnnlt  40243  islpln5  40255  lplni2  40257  lvolex3N  40258  lplnnle2at  40261  islpln2a  40268  lplnribN  40271  lplnexllnN  40284  lplnnlt  40285  lvoli3  40297  islvol5  40299  lvoli2  40301  lvolnle3at  40302  islvol2aN  40312  4atlem11  40329  lvolnltN  40338  dalawlem15  40605  4atexlemex2  40791  4atex  40796  4atex2-0aOLDN  40798  4atex2-0cOLDN  40800  lautcvr  40812  ltrnfset  40837  ltrnset  40838  ltrnu  40841  trlfset  40880  trlset  40881  trlval2  40883  cdlemd6  40923  cdleme0nex  41010  cdleme18d  41015  cdleme25b  41074  cdleme25cv  41078  cdleme29b  41095  cdleme31fv  41110  cdleme31fv2  41113  cdlemefrs29bpre0  41116  cdlemefr32sn2aw  41124  cdlemefr29bpre0N  41126  cdlemefr29clN  41127  cdlemefr32fvaN  41129  cdlemefr32fva1  41130  cdlemefs32sn1aw  41134  cdleme32fva  41157  cdleme32fvaw  41159  cdleme40v  41189  cdleme42b  41198  cdleme46f2g2  41213  cdleme46f2g1  41214  cdleme48gfv  41257  cdlemg1fvawlemN  41293  cdlemg1cex  41308  cdlemg6d  41341  cdlemm10N  41838  dicffval  41894  dicfval  41895  dicval  41896  dicfnN  41903  dicvalrelN  41905  dihffval  41950  dihfval  41951  dihlsscpre  41954  dvh4dimat  42158  dvh3dimatN  42159  dvh4dimlem  42163  dvh3dim  42166  dvh4dimN  42167  dvh3dim2  42168  dvh3dim3N  42169  mapdcv  42380  mapdh9aOLDN  42510  hdmapfval  42547  hdmapval  42548  hdmapval2  42552  hdmap11lem2  42562  dvrelog2b  42779  aks4d1p4  42792  aks4d1p5  42793  aks4d1p7  42796  aks4d1p8d2  42798  aks4d1p8  42800  aks4d1  42802  aks6d1c2p2  42832  hashnexinj  42841  rspcsbnea  42844  aks6d1c5  42852  aks6d1c6lem3  42885  aks6d1c7  42897  supinf  42956  oexpreposd  43029  mullt0b2d  43204  flt4lem7  43339  nna4b4nsq  43340  ellz1  43446  rencldnfilem  43495  jm2.22  43670  jm2.23  43671  wepwsolem  43717  fnwe2lem2  43726  aomclem8  43736  unxpwdom3  43770  onsupmaxb  43914  onexlimgt  43918  onsupeqnmax  43922  onov0suclim  43949  oaordnr  43971  omnord1  43980  oenord1  43991  oaomoencom  43992  oenass  43994  cantnfresb  43999  tfsnfin  44027  ralopabb  44085  nlimsuc  44115  ifpbi12  44162  dfsucon  44197  sqrtcvallem1  44305  ss2iundf  44333  frege124d  44435  clsk3nimkb  44714  clsk1indlem1  44719  clsk1independent  44720  ntrneineine1lem  44758  ntrneicls11  44764  clsneiel1  44782  clsneiel2  44783  neicvgel1  44793  neicvgel2  44794  radcnvrat  44972  rusbcALT  45096  en3lpVD  45501  0elaxnul  45640  omssaxinf2  45645  permaxnul  45665  permaxinf2lem  45669  nregmodel  45674  eliin2f  45770  nssd  45771  wessf1ornlem  45851  rexanuz2nf  46154  limsupre2lem  46386  icccncfext  46549  stoweidlem14  46676  stoweidlem34  46696  stoweidlem59  46721  etransclem24  46920  nnfoctbdjlem  47117  nnfoctbdj  47118  hspmbllem2  47289  nsssmfmbflem  47440  fsetsnprcnex  47737  eu2ndop1stv  47807  afvfv0bi  47834  afvco2  47858  ndmaovg  47866  ndfatafv2nrn  47903  afv2ndefb  47906  afv2fv0  47947  nelbr  47956  otiunsndisjX  47961  fun2dmnopgexmpl  47966  ltnltne  47981  readdcnnred  47985  resubcnnred  47986  recnmulnred  47987  cndivrenred  47988  ichnreuop  48166  nprmmul1  48221  fmtnoinf  48233  odz2prm2pw  48260  prmdvdsfmtnof1lem2  48282  lighneallem3  48304  lighneallem4  48307  requad1  48332  isodd3  48362  bits0ALTV  48389  nfermltl8rev  48452  nfermltl2rev  48453  nfermltlrev  48454  upgrimpths  48619  isubgr3stgrlem3  48678  usgrexmpl12ngric  48748  pgnbgreunbgrlem2lem1  48824  pgnbgreunbgrlem2lem2  48825  pgnbgreunbgrlem2lem3  48826  pgnbgreunbgrlem5lem1  48830  pgnbgreunbgrlem5lem2  48831  pgnbgreunbgrlem5lem3  48832  lgricngricex  48839  lidldomnnring  48946  smprngprmrng  49049  ztprmneprm  49072  lindepsnlininds  49177  islindeps  49178  lindslinindsimp2lem5  49187  lindslinindsimp2  49188  line2ylem  49476  line2xlem  49478  map0cor  49578  nelsubc3lem  49793  fulltermc2  50235  setc1onsubc  50325  cnelsubclem  50326  elsetrecslem  50422