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  1554  equsexvw  2037  cbvexvw  2069  cbvexdvaw  2071  excomimw  2076  hbe1w  2082  19.8aw  2084  exexw  2085  ru0  2163  cbvexv1  2371  cbvex2v  2373  drex1v  2399  cbvex  2428  cbvex2  2441  drex1  2470  eujustALT  2597  necon3abid  2991  neleq12d  3066  cbvrexdva  3243  cbvrexfw  3303  cbvrexdva2  3337  cbvrexf  3346  cbvexeqsetf  3465  ceqsex  3497  ceqsexv  3498  gencbval  3508  spcegf  3546  spc2gv  3554  spc2d  3556  spc3gv  3558  ceqsralbv  3610  cdeqnot  3725  rru  3736  sbcng  3785  sbcrext  3819  cbvrexcsf  3889  dfpss3  4016  difjust  4046  eldif  4049  difeq2  4057  disjne  4407  pssdifcom1  4444  eldifpr  4618  rexsng  4636  elpwunsn  4644  eldiftp  4647  rexprg  4657  preqsnd  4818  disjxun  5100  exnelv  5266  nalsetOLD  5268  dtruALT2  5331  dtruALT  5349  rexxfrd  5370  rexxfr2d  5372  rexxfrd2  5374  rexxfr  5377  opthneg  5449  snopeqop  5477  otiunsndisj  5492  poeq1  5561  pocl  5566  swopo  5569  sotric  5588  sotrieq  5589  isso2i  5595  somo  5597  freq1  5617  frirr  5626  fr2nr  5627  frminex  5629  tz7.2  5633  wereu2  5647  poinxp  5731  frinxp  5733  posn  5736  frsn  5738  rexiunxp  5816  rexxpf  5824  intirr  6111  poirr2  6117  cnvpo  6290  dfpo2  6299  predpoirr  6336  predfrirr  6337  frpomin  6343  nordeq  6381  ordtri1  6396  ordtri3  6399  fvmpti  6992  fndmdif  7041  rexrnmptw  7095  rexrnmpt  7097  rexima  7244  f1imapss  7270  f1ounsn  7280  cbvexfo  7298  nf1const  7312  soisoi  7336  isopolem  7353  weniso  7364  canth  7374  riotaclb  7418  rexrnmpo  7560  ndmovg  7604  sorpssuni  7748  sorpssint  7749  fr3nr  7786  dfwe2  7788  ordsucsssuc  7834  nlimsucg  7853  orduninsuc  7854  dfom2  7879  ssnlim  7897  resf1extb  7946  f1oweALT  7984  frxp  8138  poxp  8140  fnwe2lem3  8147  frxp2  8161  frxp3  8168  xpord3inddlem  8171  soseq  8176  suppofssd  8220  suppcoss  8224  smoword  8374  tz7.48lemOLD  8451  oacan  8556  oaword  8557  omlimcl  8586  omeulem1  8590  nnaword  8636  nnmword  8642  nneob  8665  naddss1  8699  brdifun  8748  swoer  8749  undifixp  8962  boxcutc  8969  2dom  9058  php  9222  phpeqd  9227  nndomog  9228  onomeneq  9229  nnsdomo  9234  unxpdomlem2  9248  frfi  9276  unfilem1  9297  tfsnfin2  9352  supeq3  9441  supeq123d  9442  supmo  9444  eqsup  9448  supub  9451  sup0  9459  suppr  9464  supisolem  9466  supisoex  9467  eqinf  9477  infval  9479  infmo  9489  infpr  9497  infempty  9501  oieq1  9506  ordtypecbv  9511  ordtypelem7  9518  wemapsolem  9544  canthwdom  9573  zfregcl  9588  zfregclOLD  9589  elirrv  9591  elirrvOLD  9592  elirrvOLDOLD  9593  elirr  9594  noinfep  9661  cantnfp1lem3  9681  ttrcltr  9717  rankr1clem  9829  carden2b  10048  domtri2  10070  alephord3  10157  alephdom2  10166  alephval3  10189  dfac9  10215  kmlem2  10230  kmlem4  10232  isfin4  10375  isfin7  10379  fin23lem11  10395  isf32lem5  10435  isf34lem4  10455  fin1a2lem6  10483  fin1a2lem7  10484  fin1a2lem12  10489  itunisuc  10497  ac6n  10563  zorn2g  10581  zornn0g  10583  ttukeylem7  10593  infinfg  10650  axpowndlem3  10684  axpowndlem4  10685  axregnd  10689  elgch  10707  engch  10713  fpwwe2lem12  10727  fpwwe2  10728  pwfseqlem1  10743  pwfseqlem3  10745  hargch  10758  addnidpi  10986  pinq  11012  nqereu  11014  ltsonq  11054  prlem934  11118  ltexprlem7  11127  addcanpr  11131  prlem936  11132  reclem2pr  11133  reclem3pr  11134  supexpr  11139  ltsosr  11179  supsrlem  11196  axpre-lttri  11250  axpre-sup  11254  xrlenlt  11374  axlttri  11381  axsup  11385  ltne  11407  dedekind  11473  readdcan  11484  leadd1  11784  ltsub1  11812  ltsub2  11813  leord1  11843  lediv1  12182  lemuldiv  12197  lerec  12200  le2msq  12217  infm3  12276  suprnub  12282  infregelb  12301  avgle1  12586  avgle2  12587  znnnlt1  12723  indstr  13043  zsupss  13064  uzsupss  13067  rpneg  13154  xralrple  13335  xleneg  13348  xltadd1  13386  xposdif  13392  xmulneg1  13399  xltmul1  13422  xrsupexmnf  13435  xrinfmexpnf  13436  xrsupsslem  13437  xrinfmsslem  13438  xrub  13442  supxrleub  13456  infxrgelb  13466  difreicc  13615  nn0disj  13778  nelfzo  13799  elfznelfzo  13908  fvinim0ffz  13924  injresinjlem  13925  ssnn0fi  14128  leexp2  14314  exp11nnd  14405  hashbnd  14480  hasheni  14492  hashfundm  14587  hashbc  14598  wrdsymb0  14694  swrdnd  14804  swrdnd2  14805  pfxnd0  14838  repswswrd  14935  repswccat  14937  cshwidxmod  14954  cnpart  15407  sqrtlt  15428  limsuplt  15646  rlimrege0  15746  isercoll  15835  efle  16286  odd2np1  16511  sumodd  16558  divalglem7  16569  ndvdsadd  16580  fldivndvdslt  16586  bitsfval  16593  bitsval  16594  bits0  16598  bitsp1  16601  bitsmod  16606  bitscmp  16608  bitsinv1lem  16611  sadadd2lem2  16620  saddisjlem  16634  bitsshft  16645  gcdneg  16694  algcvgblem  16752  lcmneg  16778  isprm3  16858  dvdsnprmd  16865  isprm5  16883  rpexp  16898  phiprmpw  16953  m1dvdsndvds  16976  pythagtrip  17012  pcgcd1  17055  prmpwdvds  17082  prmreclem2  17095  prmreclem3  17096  prmreclem5  17098  prmreclem6  17099  vdwlem6  17164  vdwnnlem2  17174  vdwnnlem3  17175  vdwnn  17176  prmlem0  17283  prmlem1a  17284  divsfval  17719  mrisval  17804  ismri  17805  ismri2dad  17811  cidpropd  17884  cat1lem  18271  plttr  18514  joinval  18549  meetval  18563  acsfiindd  18727  isnsgrp  18912  smndex1n0mnd  19111  mgm2nsgrplem2  19118  sgrp2nmndlem3  19124  degenmgm2nfun  19139  symgpssefmnd  19610  symgfix2  19630  pmtrdifellem4  19693  psgnunilem1  19707  psgnunilem5  19708  psgnunilem2  19709  psgnunilem3  19710  pmtrsn  19733  sylow1lem3  19814  sylow2alem2  19832  efgsfo  19953  ablfac1eulem  20288  ablfac1eu  20289  pgpfac1lem1  20290  pgpfac1lem5  20295  nzrunit  20775  zrninitoringc  20928  islbs  21351  lbsind  21355  lbspss  21357  lbspropd  21374  lspsnne1  21395  islbs2  21432  lbsacsbs  21434  lbsextlem1  21436  lbsextlem3  21438  lbsextlem4  21439  lbsextg  21440  ssdifidlprm  21642  frlmlbs  22103  islindf  22118  islinds2  22119  islindf2  22120  lindfind  22122  lindsind  22123  lindfrn  22127  lindfmm  22133  lsslindf  22136  islindf4  22144  lindsenlbs  22157  opsrtoslem2  22365  psdmul  22487  cply1coe0  22619  cply1coe0bi  22620  mdetunilem7  22933  mdetunilem8  22934  mdetunilem9  22935  maducoeval2  22955  matunitlindflem1  22994  pmatcollpw3fi1lem1  23104  fvmptnn04ifa  23168  fvmptnn04ifc  23170  fvmptnn04ifd  23171  chfacffsupp  23174  chfacfscmul0  23176  chfacfpmmul0  23180  elcls  23391  maxlp  23465  perfi  23473  ordtbaslem  23506  ordtval  23507  ordtbas2  23509  ordtopn1  23512  ordtopn2  23513  ordtcnv  23519  ordtrest  23520  ordtrest2lem  23521  ordtrest2  23522  pnfnei  23538  mnfnei  23539  isreg2  23695  ordthauslem  23701  cmpfi  23726  cmpfii  23727  bwth  23728  nconnsubb  23741  hausdiag  23964  txkgen  23971  kqdisj  24051  ordthmeolem  24120  fbfinnfr  24160  trfbas  24163  fbunfip  24188  fbasrn  24203  trfil3  24207  ufileu  24238  fin1aufil  24251  hausflim  24300  alexsubALTlem2  24367  alexsubALTlem3  24368  alexsubALTlem4  24369  ptcmplem2  24372  ptcmplem3  24373  stdbdbl  24836  iccntr  25141  reconnlem2  25147  iccpnfcnv  25265  xrhmeo  25267  lebnumlem1  25282  lebnumlem2  25283  lebnumlem3  25284  bcthlem4  25648  minveclem3b  25749  ivthlem2  25773  ivthlem3  25774  mbfmax  25970  mbfposr  25973  i1fd  26002  mbfi1fseqlem4  26039  itg2splitlem  26069  itg2monolem1  26071  itg2cnlem1  26082  dvne0  26331  lhop1lem  26333  deg1nn0clb  26408  dgrle  26562  coemulhi  26573  plymulidp  26603  aaliou3lem9  26677  cos11  26861  logleb  26931  argrege0  26939  logdivle  26950  ellogdm  26967  cxple  27023  cxplt2  27026  cxple3  27029  isosctrlem1  27146  atandm  27204  atans2  27259  atantayl2  27266  eldmgm  27349  ftalem7  27406  isppw2  27442  musum  27518  dchrsum2  27595  bposlem1  27611  lgsmod  27650  lgsdir2lem2  27653  lgsdir2  27657  lgsne0  27662  lgsprme0  27666  gausslemma2dlem4  27696  lgsquadlem1  27707  2lgslem3  27731  2lgsoddprm  27743  2sq2  27760  addsqrexnreu  27769  rpvmasumlem  27814  padicabv  27957  ostth3  27965  ostth  27966  flt4lem7  27989  nna4b4nsq  27990  noextenddif  28025  nodenselem4  28044  nodenselem5  28045  nodenselem7  28047  nolt02o  28052  nogt01o  28053  noresle  28054  nosupprefixmo  28057  noinfprefixmo  28058  nosupcbv  28059  nosupdm  28061  nosupfv  28063  nosupres  28064  nosupbnd1lem1  28065  nosupbnd1lem3  28067  nosupbnd1lem5  28069  nosupbnd1  28071  nosupbnd2lem1  28072  nosupbnd2  28073  noinfcbv  28074  noinfdm  28076  noinffv  28078  noinfres  28079  noinfbnd1lem1  28080  noinfbnd1lem3  28082  noinfbnd1lem5  28084  noinfbnd1  28086  noinfbnd2lem1  28087  noinfbnd2  28088  lenlts  28109  ltsne  28131  nocvxminlem  28140  lesrec  28185  eqcuts3  28190  cuteq1  28203  newbday  28288  ltslpss  28294  cofcutr  28310  lrrecfr  28329  addsval  28348  ltadds2  28377  lenegs  28432  lesubsubsbd  28472  lesubsubs2bd  28473  lesubsubs3bd  28474  lesubaddsd  28479  ltmuls2  28557  lemuls2d  28560  lemuls1d  28561  oncutlt  28650  onles  28654  pw2cut2  28848  bdaypw2bnd  28851  bdayfinbndlem1  28853  istrkgld  28921  axtgupdim2  28933  tglowdim2l  29119  axlowdimlem16  29535  axlowdim2  29538  axlowdim  29539  numedglnl  29722  usgredg2v  29808  lfuhgr1v0e  29835  cusgrfi  30039  vtxd0nedgb  30069  vtxduhgr0edgnel  30075  1loopgrnb0  30083  1hevtxdg0  30086  vtxdgoddnumeven  30134  wlkp1lem1  30252  wlkp1lem2  30253  wlkp1lem5  30256  revwlk  30267  dfpth2  30314  crctcsh  30413  clwlkclwwlklem2a4  30588  isacycgr  30751  eupth2eucrct  30818  eupth2lem3lem3  30831  eupth2lem3lem4  30832  eupth2lem3lem6  30834  eupth2lem3lem7  30835  eupth2lems  30839  eupth2  30840  konigsberglem4  30856  nfrgr2v  30873  frgrwopreglem3  30915  fusgr2wsp2nb  30935  frgrreggt1  30994  friendshipgt3  30999  lpni  31082  nmobndseqi  31381  minvecolem5  31483  chpsscon3  32105  chnle  32116  nonbooli  32253  pjnel  32328  specval  32500  nmcfnlbi  32654  stri  32859  hstri  32867  cvbr  32884  cvcon3  32886  chcv1  32957  cvexchlem  32970  chrelat2  32972  nelun  33109  elpreq  33124  nelpr  33127  ifeqeqx  33138  nfpconfp  33226  suppiniseg  33279  isoun  33295  suppss3  33315  xrge0infss  33352  infxrge0gelb  33358  eliccelico  33369  elicoelioo  33370  nndiffz1  33378  hashgt1  33400  expgt0b  33408  nn0min  33412  ccatws1f1o  33514  toslublem  33533  tosglblem  33535  pmtrcnel  33650  cycpmco2  33694  isarchi2  33746  archiabl  33759  elrgspnlem2  33804  elrgspnlem3  33805  0nellinds  33926  lindssn  33933  lindfpropd  33937  mxidlirred  33997  ssmxidl  33999  dflringlem  34026  esplyind  34207  lbslsat  34248  lindsunlem  34256  rtelextdg2lem  34358  constrsqrtcl  34411  ordtcnvNEW  34552  ordtrestNEW  34553  ordtrest2NEWlem  34554  ordtrest2NEW  34555  ordtconnlem1  34556  xrge0iifcnv  34565  esumpcvgval  34710  esum2d  34725  ddemeas  34869  omssubadd  34932  oddpwdc  34986  eulerpartlems  34992  eulerpartlemf  35002  eulerpartlemt  35003  eulerpartlemr  35006  eulerpartlemgvv  35008  eulerpartlemn  35013  ballotlemfc0  35125  ballotlemfcc  35126  ballotlem4  35131  ballotlemimin  35138  ballotlem7  35168  signsply0  35180  reprinfz1  35251  reprpmtf1o  35255  reprdifc  35256  hgt750lema  35286  hgt750leme  35287  istrkg2d  35295  bnj23  35349  bnj1185  35423  bnj1228  35641  bnj1388  35663  bnj1417  35671  ordtypeon  35719  nummin  35722  axprALT2  35734  infinfnum  35757  fineqvnttrclselem1  35789  axnulg  35813  onvf1odlem2  35883  onvf1odlem3  35884  acycgr0v  35913  prclisacycgr  35916  erdszelem10  35965  satf0n0  36143  fmlaomn0  36155  fmlasucdisj  36164  satfv1fvfmla1  36188  satefvfmla1  36190  ismfs  36314  mvtinf  36320  untelirr  36473  untsucf  36475  untangtr  36479  dfon2lem3  36547  dfon2lem4  36548  dfon2lem7  36551  dfon2lem9  36553  distel  36565  funpartfv  36709  dfrdg4  36715  nmulprop  36939  naddle  36968  nn0prpwlem  37110  nn0prpw  37111  limsucncmpi  37233  limsucncmp  37234  ordcmp  37235  weiunlem  37251  weiunfrlem  37252  weiunfr  37255  axtcond  37266  regsfromregtco  37326  regsfromsetind  37327  unblimceq0  37373  unbdqndv1  37374  bj-hbntbi  37606  bj-equsexvwd  37675  bj-cbvexdv  37712  bj-ru1  37856  bj-nuliota  37972  topdifinffinlem  38271  topdifinffin  38272  icorempo  38275  relowlpssretop  38288  finxpreclem2  38314  finxpreclem6  38320  wl-issetft  38515  wl-eujustlem1  38521  leceifl  38533  lindsadd  38537  poimirlem16  38555  poimirlem17  38556  poimirlem18  38557  poimirlem19  38558  poimirlem21  38560  poimirlem23  38562  poimirlem26  38565  poimirlem27  38566  poimirlem28  38567  poimirlem31  38570  poimir  38572  mblfinlem2  38577  mblfinlem3  38578  ismblfin  38580  cnambfre  38587  itg2addnclem  38590  itg2addnclem2  38591  iblabsnclem  38602  ftc1anclem1  38612  areacirc  38632  heibor1lem  38744  heiborlem1  38746  heiborlem6  38751  heiborlem8  38753  heiborlem10  38755  smprngopr  38987  ecin0  39285  ax12inda  40006  riotaclbgBAD  40012  lcvfbr  40078  lcvbr  40079  lsatcv0  40089  l1cvpat  40112  opltcon3b  40262  cvrfval  40326  cvrval  40327  cvrnbtwn  40329  cvrval2  40332  cvrnbtwn2  40333  cvrnbtwn3  40334  cvrcon3b  40335  cvrnbtwn4  40337  atnlt  40371  iscvlat  40381  cvlexch1  40386  hlsuprexch  40439  hlrelat5N  40459  hlrelat2  40461  cvrval5  40473  3dimlem1  40516  3dim1lem5  40524  3dim2  40526  3dim3  40527  llnnlt  40581  islpln5  40593  lplni2  40595  lvolex3N  40596  lplnnle2at  40599  islpln2a  40606  lplnribN  40609  lplnexllnN  40622  lplnnlt  40623  lvoli3  40635  islvol5  40637  lvoli2  40639  lvolnle3at  40640  islvol2aN  40650  4atlem11  40667  lvolnltN  40676  dalawlem15  40943  4atexlemex2  41129  4atex  41134  4atex2-0aOLDN  41136  4atex2-0cOLDN  41138  lautcvr  41150  ltrnfset  41175  ltrnset  41176  ltrnu  41179  trlfset  41218  trlset  41219  trlval2  41221  cdlemd6  41261  cdleme0nex  41348  cdleme18d  41353  cdleme25b  41412  cdleme25cv  41416  cdleme29b  41433  cdleme31fv  41448  cdleme31fv2  41451  cdlemefrs29bpre0  41454  cdlemefr32sn2aw  41462  cdlemefr29bpre0N  41464  cdlemefr29clN  41465  cdlemefr32fvaN  41467  cdlemefr32fva1  41468  cdlemefs32sn1aw  41472  cdleme32fva  41495  cdleme32fvaw  41497  cdleme40v  41527  cdleme42b  41536  cdleme46f2g2  41551  cdleme46f2g1  41552  cdleme48gfv  41595  cdlemg1fvawlemN  41631  cdlemg1cex  41646  cdlemg6d  41679  cdlemm10N  42176  dicffval  42232  dicfval  42233  dicval  42234  dicfnN  42241  dicvalrelN  42243  dihffval  42288  dihfval  42289  dihlsscpre  42292  dvh4dimat  42496  dvh3dimatN  42497  dvh4dimlem  42501  dvh3dim  42504  dvh4dimN  42505  dvh3dim2  42506  dvh3dim3N  42507  mapdcv  42718  mapdh9aOLDN  42848  hdmapfval  42885  hdmapval  42886  hdmapval2  42890  hdmap11lem2  42900  dvrelog2b  43117  aks4d1p4  43130  aks4d1p5  43131  aks4d1p7  43134  aks4d1p8d2  43136  aks4d1p8  43138  aks4d1  43140  aks6d1c2p2  43170  hashnexinj  43179  rspcsbnea  43182  aks6d1c5  43190  aks6d1c6lem3  43223  aks6d1c7  43235  supinf  43294  oexpreposd  43380  mullt0b2d  43549  ellz1  43778  rencldnfilem  43827  jm2.22  44002  jm2.23  44003  wepwsolem  44049  aomclem8  44063  unxpwdom3  44097  onsupmaxb  44241  onexlimgt  44245  onsupeqnmax  44249  onov0suclim  44276  oaordnr  44298  omnord1  44307  oenord1  44318  oaomoencom  44319  oenass  44321  cantnfresb  44326  tfsnfin  44354  ralopabb  44412  nlimsuc  44442  ifpbi12  44489  dfsucon  44524  sqrtcvallem1  44631  ss2iundf  44659  frege124d  44761  clsk3nimkb  45040  clsk1indlem1  45045  clsk1independent  45046  ntrneineine1lem  45084  ntrneicls11  45090  clsneiel1  45108  clsneiel2  45109  neicvgel1  45119  neicvgel2  45120  radcnvrat  45298  rusbcALT  45422  en3lpVD  45827  0elaxnul  45973  omssaxinf2  45978  permaxnul  45998  permaxinf2lem  46002  nregmodel  46007  eliin2f  46119  nssd  46120  wessf1ornlem  46200  rexanuz2nf  46502  limsupre2lem  46734  icccncfext  46897  stoweidlem14  47024  stoweidlem34  47044  stoweidlem59  47069  etransclem24  47268  nnfoctbdjlem  47465  nnfoctbdj  47466  hspmbllem2  47637  nsssmfmbflem  47788  fsetsnprcnex  48125  eu2ndop1stv  48195  afvfv0bi  48222  afvco2  48246  ndmaovg  48254  ndfatafv2nrn  48291  afv2ndefb  48294  afv2fv0  48335  nelbr  48344  otiunsndisjX  48349  fun2dmnopgexmpl  48354  ltnltne  48369  readdcnnred  48373  resubcnnred  48374  recnmulnred  48375  cndivrenred  48376  ichnreuop  48554  nprmmul1  48609  fmtnoinf  48621  odz2prm2pw  48648  prmdvdsfmtnof1lem2  48670  lighneallem3  48692  lighneallem4  48695  requad1  48720  isodd3  48750  bits0ALTV  48777  nfermltl8rev  48840  nfermltl2rev  48841  nfermltlrev  48842  upgrimpths  49007  isubgr3stgrlem3  49066  usgrexmpl12ngric  49136  pgnbgreunbgrlem2lem1  49212  pgnbgreunbgrlem2lem2  49213  pgnbgreunbgrlem2lem3  49214  pgnbgreunbgrlem5lem1  49218  pgnbgreunbgrlem5lem2  49219  pgnbgreunbgrlem5lem3  49220  lgricngricex  49227  lidldomnnring  49333  smprngprmrng  49436  ztprmneprm  49459  lindepsnlininds  49564  islindeps  49565  lindslinindsimp2lem5  49574  lindslinindsimp2  49575  line2ylem  49863  line2xlem  49865  map0cor  49965  nelsubc3lem  50178  fulltermc2  50620  setc1onsubc  50710  cnelsubclem  50711  elsetrecslem  50792