Theorem oveq2d 6101

Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)

Hypothesis

Ref	Expression
oveq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
oveq2d	|- ( ph -> ( C F A ) = ( C F B ) )

Proof of Theorem oveq2d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 |- ( ph -> A = B )
2		oveq2 6093	. 2 |- ( A = B -> ( C F A ) = ( C F B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C F A ) = ( C F B ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  csbov1g  6126  caovassg  6248  caovdig  6264  caovdirg  6267  caov32d  6270  caov4d  6274  caov42d  6276  suppofss1dcl  6504  suppofss2dcl  6505  nnaass  6758  nndi  6759  nnmass  6760  nnmsucr  6761  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  addasspig  7698  mulasspig  7700  distrpig  7701  dfplpq2  7722  mulpipq2  7739  addassnqg  7750  prarloclemarch  7786  prarloclemarch2  7787  ltrnqg  7788  enq0sym  7800  addnq0mo  7815  mulnq0mo  7816  addnnnq0  7817  nq0a0  7825  distrnq0  7827  addassnq0  7830  prarloclemlo  7862  prarloclem3  7865  prarloclem5  7868  prarloclemcalc  7870  addnqprl  7897  addnqpru  7898  prmuloclemcalc  7933  mulnqprl  7936  mulnqpru  7937  distrlem4prl  7952  distrlem4pru  7953  1idprl  7958  1idpru  7959  ltexprlemloc  7975  addcanprleml  7982  addcanprlemu  7983  recexprlem1ssu  8002  ltmprr  8010  caucvgprlemcanl  8012  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  cauappcvgprlem1  8027  cauappcvgprlemlim  8029  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemdisj  8042  caucvgprlemloc  8043  caucvgprlemcl  8044  caucvgprlemladdrl  8046  caucvgprlem1  8047  caucvgpr  8050  caucvgprprlemell  8053  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemnkeqj  8058  caucvgprprlemopl  8065  caucvgprprlemlol  8066  caucvgprprlemloc  8071  caucvgprprlemclphr  8073  caucvgprprlemexb  8075  caucvgprprlemaddq  8076  caucvgprprlem1  8077  addcmpblnr  8107  mulcmpblnrlemg  8108  addsrmo  8111  mulsrmo  8112  addsrpr  8113  mulsrpr  8114  ltsrprg  8115  recexgt0sr  8141  mulgt0sr  8146  caucvgsrlemgt1  8163  caucvgsrlemoffval  8164  caucvgsr  8170  suplocsrlemb  8174  suplocsrlempr  8175  suplocsrlem  8176  suplocsr  8177  mulcnsr  8203  pitoregt0  8217  recidpirqlemcalc  8225  axmulcom  8239  axmulass  8241  axdistr  8242  ax0id  8246  axcnre  8249  recriota  8258  axcaucvglemcau  8266  axcaucvglemres  8267  mulrid  8324  adddirp1d  8353  mul32  8458  mul31  8459  add32  8487  add4  8489  add42  8490  cnegex  8506  addcan2  8509  addsubass  8538  subsub2  8556  nppcan2  8559  sub32  8562  nnncan  8563  sub4  8573  muladd  8713  subdi  8714  mul2neg  8727  submul2  8728  mulsub  8730  muls1d  8747  mulsubfacd  8748  add20  8804  recexre  8909  rereim  8917  apreap  8918  ltmul1  8923  cru  8933  apreim  8934  mulreim  8935  apadd1  8939  apneg  8942  mulap0  8985  divrecap  9021  divassap  9023  divmulasscomap  9029  divsubdirap  9041  divdivdivap  9046  divmul24ap  9049  divmuleqap  9050  divcanap6  9052  divdivap1  9056  divdivap2  9057  divsubdivap  9061  conjmulap  9062  div2negap  9068  apmul1  9121  cju  9294  nnmulcl  9328  add1p1  9560  sub1m1  9561  cnm2m1cnm3  9562  xp1d2m1eqxm1d2  9563  div4p1lem1div2  9564  un0addcl  9601  un0mulcl  9602  zaddcllemneg  9688  qapne  10049  cnref1o  10062  rexsub  10266  xnegid  10272  xaddcom  10274  xnegdi  10281  xaddass  10282  xaddass2  10283  xpncan  10284  xnpcan  10285  xleadd1a  10286  xsubge0  10294  xposdif  10295  xlesubadd  10296  xadd4d  10298  lincmb01cmp  10416  iccf1o  10418  ige3m2fz  10465  fztp  10496  fzsuc2  10497  fseq1m1p1  10513  fzm1  10518  ige2m1fz1  10527  nn0split  10554  nnsplit  10555  fzo0addelr  10618  elfzoext  10621  fzval3  10633  zpnn0elfzo1  10637  fzosplitsnm1  10638  fzosplitpr  10663  fzosplitprm1  10664  fzoshftral  10668  rebtwn2zlemstep  10698  flhalf  10751  fldiv4lem1div2uz2  10755  modqval  10775  modqvalr  10776  modqdiffl  10786  modqfrac  10788  flqmod  10789  intqfrac  10790  zmod10  10791  modqmulnn  10793  modqvalp1  10794  modqid  10800  modqcyc  10810  modqcyc2  10811  modqmul1  10828  q2submod  10836  modqdi  10843  modqsubdir  10844  modqeqmodmin  10845  modsumfzodifsn  10847  addmodlteq  10849  frecuzrdgsuctlem  10874  uzsinds  10895  seqeq3  10903  iseqvalcbv  10910  seq3val  10911  seqvalcd  10912  seqf  10915  seq3p1  10916  seqovcd  10918  seqp1cd  10921  seq3m1  10924  seq3fveq2  10926  seqfveq2g  10928  seq3shft2  10932  seqshft2g  10933  monoord2  10937  ser3mono  10938  seq3split  10939  seqsplitg  10940  seq3caopr3  10942  seqcaopr3g  10943  seq3caopr2  10944  seqcaopr2g  10945  seq3caopr  10946  seqcaoprg  10947  seqf1oglem2a  10969  seqf1oglem2  10971  seq3id2  10977  seq3homo  10978  seq3z  10979  seqhomog  10981  exp3vallem  10991  exp3val  10992  expp1  10997  expnegap0  10998  expineg2  10999  expn1ap0  11000  expm1t  11018  1exp  11019  expnegzap  11024  mulexpzap  11030  expadd  11032  expaddzaplem  11033  expaddzap  11034  expmul  11035  expmulzap  11036  m1expeven  11037  expsubap  11038  expp1zap  11039  expm1ap  11040  expdivap  11041  iexpcyc  11095  subsq2  11098  binom2  11102  binom21  11103  binom2sub  11104  binom2sub1  11105  mulbinom2  11107  binom3  11108  zesq  11110  bernneq  11112  sqoddm1div8  11145  mulsubdivbinom2ap  11164  nn0opthlem1d  11173  nn0opthd  11175  facp1  11183  facnn2  11187  faclbnd  11194  faclbnd6  11197  bcval  11202  bccmpl  11207  bcn0  11208  bcnn  11210  bcnp1n  11212  bcm1k  11213  bcp1n  11214  bcp1nk  11215  bcval5  11216  bcp1m1  11218  bcpasc  11219  bcm1n  11222  bcn2m1  11223  bcn2p1  11224  omgadd  11257  hashunlem  11259  hashunsng  11263  hashdifsn  11275  hashxp  11282  hashmap  11283  sseqn  11294  hashf1lem2  11301  hashf1  11302  hashfac  11303  zfz1isolemsplit  11305  zfz1isolem1  11307  zfz1iso  11308  seq3coll  11309  wrdf  11325  ccatfvalfi  11375  elfzelfzccat  11383  ccatlid  11389  ccatrid  11390  ccatass  11391  ccatalpha  11396  ccatws1leng  11417  ccats1val2  11423  ccatw2s1p1g  11428  swrdval  11435  swrd00g  11436  swrdf  11442  swrdfv2  11450  swrdwrdsymbg  11451  swrdspsleq  11454  swrds1  11455  swrdlsw  11456  ccatswrd  11457  swrdccat2  11458  pfxmpt  11467  pfxfv  11471  pfxeq  11483  pfxsuff1eqwrdeq  11486  ccatpfx  11488  pfxccat1  11489  swrdswrd  11492  pfxswrd  11493  swrdpfx  11494  pfxpfx  11495  pfxlswccat  11500  ccats1pfxeq  11501  ccats1pfxeqrex  11502  ccatopth2  11504  cats1un  11508  wrdind  11509  wrd2ind  11510  swrdccatfn  11511  swrdccatin1  11512  pfxccatin12lem4  11513  swrdccatin2  11516  pfxccatin12lem2c  11517  pfxccatin12lem2  11518  pfxccatin12  11520  swrdccat  11522  swrdccat3blem  11526  swrdccat3b  11527  swrdccatin2d  11531  pfxccatin12d  11532  reuccatpfxs1lem  11533  reuccatpfxs1  11534  shftcan1  11614  shftcan2  11615  cjval  11625  cjth  11626  crre  11637  replim  11639  remim  11640  reim0b  11642  rereb  11643  mulreap  11644  cjreb  11646  recj  11647  reneg  11648  readd  11649  resub  11650  remullem  11651  imcj  11655  imneg  11656  imadd  11657  imsub  11658  cjcj  11663  cjadd  11664  ipcnval  11666  cjmulrcl  11667  cjneg  11670  addcj  11671  cjsub  11672  sq01  11675  cnrecnv  11691  caucvgrelemcau  11761  cvg1nlemcau  11765  cvg1nlemres  11766  recvguniqlem  11775  resqrexlemover  11791  resqrexlemlo  11794  resqrexlemcalc1  11795  resqrexlemcalc3  11797  resqrexlemnm  11799  resqrexlemcvg  11800  absneg  11831  abscj  11833  sqabsadd  11836  sqabssub  11837  absmul  11850  absid  11852  absre  11859  absresq  11860  absexpzap  11862  recvalap  11879  abstri  11886  abs2dif2  11889  recan  11891  cau3lem  11896  amgm2  11900  bdtrilem  12023  xrmaxadd  12045  xrbdtri  12060  climaddc1  12113  climsubc1  12116  climcvg1nlem  12133  serf0  12136  fzf1o  12160  summodclem3  12165  summodclem2a  12166  summodc  12168  fsumsplitsn  12195  fsumm1  12201  fsumsplitsnun  12204  fsump1  12205  isummulc2  12211  fsumrev  12228  fisum0diag2  12232  fsummulc2  12233  fsumsub  12237  fsumabs  12250  telfsumo  12251  fsumparts  12255  fsumrelem  12256  fsumiun  12262  binomlem  12268  binom  12269  binom1p  12270  binom11  12271  binom1dif  12272  bcxmas  12274  isumsplit  12276  isum1p  12277  divcnv  12282  arisum2  12284  trireciplem  12285  trirecip  12286  geolim  12296  georeclim  12298  geo2sum  12299  geo2lim  12301  geoisum1c  12305  0.999...  12306  cvgratnnlemnexp  12309  cvgratnnlemmn  12310  cvgratz  12317  mertenslem2  12321  mertensabs  12322  clim2prod  12324  prodfrecap  12331  prodfdivap  12332  prodmodclem3  12360  prodmodclem2a  12361  fprodm1  12383  fprodp1  12385  fprodunsn  12389  fprodfac  12400  fprodeq0  12402  fprodconst  12405  fprodrec  12414  fproddivap  12415  fprodsplitsn  12418  ege2le3  12456  efaddlem  12459  efsub  12466  efexp  12467  eftlub  12475  efsep  12476  effsumlt  12477  ef4p  12479  tanval3ap  12499  resinval  12500  recosval  12501  efi4p  12502  efival  12517  efmival  12518  efeul  12519  sinadd  12521  cosadd  12522  tanaddap  12524  sinsub  12525  cossub  12526  sincossq  12533  sin2t  12534  cos2t  12535  cos2tsin  12536  ef01bndlem  12541  sin01bnd  12542  cos01bnd  12543  cos12dec  12553  absef  12555  absefib  12556  efieq1re  12557  demoivreALT  12559  eirraplem  12562  dvdsexp  12646  oexpneg  12662  opeo  12682  omeo  12683  m1exp1  12686  flodddiv4  12721  flodddiv4t2lthalf  12724  bitsval  12728  bitsp1  12736  bitsinv1lem  12746  bitsinv1  12747  divgcdnnr  12771  gcdaddm  12779  gcdadd  12780  gcdid  12781  modgcd  12786  gcdmultipled  12788  dvdsgcdidd  12789  bezoutlemnewy  12791  bezoutlema  12794  bezoutlemb  12795  bezoutlemex  12796  bezoutlembz  12799  absmulgcd  12812  gcdmultiple  12815  gcdmultiplez  12816  rpmulgcd  12821  rplpwr  12822  eucalginv  12852  eucalg  12855  lcmneg  12870  lcmgcdlem  12873  lcmgcd  12874  lcmid  12876  lcm1  12877  mulgcddvds  12890  qredeq  12892  divgcdcoprmex  12898  prmind2  12916  rpexp1i  12951  pwbdvdslemn  12962  pwbdvdseulemle  12964  pwbdvdseu  12965  nnmaxpwlemxy  12966  nnmaxpwlemdvds  12967  nnmaxpwlemndvds  12968  nnmaxpwlemparts  12970  2sqpwodd  12974  nn0gcdsq  12998  phiprmpw  13022  eulerthlemrprm  13029  eulerthlema  13030  eulerthlemh  13031  eulerthlemth  13032  fermltl  13034  prmdiv  13035  hashgcdlem  13038  odzdvds  13046  vfermltl  13052  modprm0  13055  nnnn0modprm0  13056  modprmn0modprm0  13057  coprimeprodsq  13058  pythagtriplem1  13066  pythagtriplem4  13069  pythagtriplem12  13076  pythagtriplem14  13078  pythagtriplem16  13080  pythagtriplem18  13082  pythagtrip  13084  pcpremul  13094  pceu  13096  pczpre  13098  pcdiv  13103  pcqmul  13104  pcqdiv  13108  pcexp  13110  pcxqcl  13113  pczdvds  13115  pczndvds  13117  pczndvds2  13119  pcid  13125  pcneg  13126  pcdvdstr  13128  pcgcd1  13129  pcgcd  13130  pc2dvds  13131  pcaddlem  13140  pcadd  13141  pcadd2  13142  pcmpt  13144  pcmpt2  13145  fldivp1  13149  pcfac  13151  pcbc  13152  expnprm  13154  prmpwdvds  13156  pockthlem  13157  pockthi  13159  4sqlem7  13185  4sqlem9  13187  4sqlem10  13188  4sqlem2  13190  4sqlem3  13191  4sqlem4  13193  mul4sqlem  13194  4sqlem11  13202  4sqlem16  13207  4sqlem17  13208  4sqlem19  13210  ballotfilemfc0  13283  ballotfilemfcc  13284  ballotfilemsv  13304  ballotfilemsima  13310  ballotfilemfrci  13322  setscomd  13444  ressvalsets  13469  strressid  13476  ressval3d  13477  ressinbasd  13479  ressressg  13480  ressabsg  13481  grpinvalem  13756  grpinva  13757  grprida  13758  isnsgrp  13772  sgrpass  13774  sgrp1  13777  sgrppropd  13779  mnd32g  13791  mnd4g  13793  mndpropd  13804  imasmnd2  13810  mhmex  13820  mhmlin  13825  gzsumwmhm  13854  grprcan  13893  grpsubval  13902  grpinvid2  13909  grpasscan2  13920  grpsubinv  13929  grpinvadd  13934  grpsubid1  13941  grpsubadd0sub  13943  grpsubadd  13944  grpsubsub  13945  grpaddsubass  13946  grppncan  13947  grpnnncan2  13953  grpsubpropd2  13961  imasgrp2  13964  mhmlem  13968  mhmid  13969  mhmmnd  13970  ghmgrp  13972  mulgnn0gzsum  13982  mulgnnp1  13984  mulgaddcomlem  13999  mulgaddcom  14000  mulginvinv  14002  mulgnn0dir  14006  mulgdirlem  14007  mulgp1  14009  mulgneg2  14010  mulgnn0ass  14012  mulgass  14013  mulgmodid  14015  mulgsubdir  14016  nmzsubg  14064  0nsg  14068  eqger  14078  qussub  14091  ghmlin  14102  ghmsub  14105  conjghm  14130  ablsub4  14168  abladdsub4  14169  ablsubsub4  14174  ablsub32  14177  ablnnncan  14178  gzsumconst  14194  gzsummhm2  14197  gzsumsnfd  14198  gzsumsplit0  14199  gsumvalfi  14203  gzsumgsum1  14204  gzsumgsum  14206  gsumsncmn  14207  gsump1  14208  gsumzfi  14209  gsumclfi  14210  gsumf1ofi  14211  gsummptfidmadd  14212  gsummptfidmadd2  14213  gsumsubmclfi  14214  gsummhm2fi  14216  gsumconstcmn  14217  prdssgrpd  14242  prdsidlem  14244  prdsmndd  14245  mgpress  14281  rngass  14289  rngdi  14290  rngdir  14291  rngrz  14296  rngmneg2  14298  rngsubdi  14301  rngsubdir  14302  rngpropd  14305  imasrng  14306  srgass  14326  srgpcomp  14345  srgpcompp  14346  srgpcomppsc  14347  srg1expzeq1  14350  ringpropd  14394  ringrz  14400  ringnegr  14408  ringmneg2  14410  ringsubdi  14412  ringsubdir  14413  ring1  14415  imasring  14420  opprrng  14433  opprring  14435  mulgass3  14442  dvdsrd  14452  unitgrp  14474  invrfvald  14480  dvr1  14496  dvrass  14497  dvrcan1  14498  dvrcan3  14499  rdivmuldivd  14502  subrginv  14596  subrgdv  14597  resrhm2b  14608  rrgsupp  14625  islmod  14678  lmodlema  14679  islmodd  14680  lmodvs0  14710  lmodvneg1  14718  lmodvsubval2  14730  lmodsubvs  14731  lmodsubdi  14732  lmodsubdir  14733  lmodprop2d  14736  rmodislmodlem  14738  rmodislmod  14739  lsssn0  14758  sraval  14825  cnfldsub  14963  gsumfsum  14974  mulgrhm  14995  mulgrhm2  14996  znval  15022  znval2  15024  znunit  15045  isassa  15053  assalem  15054  assa2ass2  15061  assapropd  15065  asclmul1  15080  asclmul2  15081  ascldimul  15082  asclpropd  15091  assamulgscmlem2  15093  asclmulg  15095  psrval  15101  mplvalcoe  15133  mplval2g  15138  restabs  15328  cnprcl2k  15359  cnrest2r  15390  ispsmet  15476  psmettri2  15481  psmetsym  15482  ismet  15497  isxmet  15498  xmettri2  15514  xmetsym  15521  xmettri3  15527  mettri3  15528  xblss2ps  15557  xblss2  15558  comet  15652  xmetxp  15660  xmetxpbl  15661  txmetcnp  15671  fsumcncntop  15720  cncfi  15731  divcncfap  15767  limccl  15812  ellimc3apf  15813  limccnpcntop  15828  limccnp2lem  15829  reldvg  15832  dvfvalap  15834  eldvap  15835  dvcj  15862  dvfre  15863  dvexp  15864  dvexp2  15865  dvrecap  15866  dvmptaddx  15872  dvmptmulx  15873  dvmptnegcn  15875  dvmptsubcn  15876  dvmptcjx  15877  dvmptfsum  15878  dveflem  15879  dvef  15880  plyconst  15898  plyaddlem1  15900  plymullem1  15901  plyadd  15904  plymul  15905  plycoeid3  15910  plycolemc  15911  plyco  15912  plycjlemc  15913  plycj  15914  plyrecj  15916  dvply1  15918  dvply2g  15919  sin0pilem1  15935  sin0pilem2  15936  efper  15961  sinperlem  15962  efimpi  15973  ptolemy  15978  tangtx  15992  abssinper  16000  cosq34lt1  16004  rpcxpef  16052  rpcxpp1  16064  rpcxpneg  16065  rpcxpsub  16066  rpmulcxp  16067  rpdivcxp  16069  cxpmul  16070  rpcxpmul2  16071  rpcxproot  16072  cxpcom  16096  rpabscxpbnd  16098  rplogbval  16103  rplogbreexp  16111  rplogbzexp  16112  rprelogbmulexp  16114  rprelogbdiv  16115  relogbexpap  16116  rplogbcxp  16121  rpcxplogb  16122  logbgcd1irr  16125  logbgcd1irraplemap  16127  zprmlogbaplem2  16138  zprmlogbap  16140  binom4  16141  log2tlbndlog2  16142  log2ublem2  16144  birthdaylem2  16148  pellexlem2  16152  pellexlem3  16153  wilthlem1  16154  ppival2  16171  ppival2g  16172  sgmval  16174  chtqfl  16180  chtprm  16183  chtnprm  16184  chtdif  16186  prmorcht  16204  sgmppw  16208  1sgmprm  16210  chtublem  16217  chtqub  16218  mersenne  16219  perfectlem1  16221  perfectlem2  16222  perfect  16223  bcctr  16224  pcbcctr  16225  bcmono  16226  bcp1ctr  16228  bposlem1  16233  bposlem2  16234  bposlem5  16237  lgslem1  16241  lgsval  16245  lgsfvalg  16246  lgsval2lem  16251  lgsval4  16261  lgsneg  16265  lgsneg1  16266  lgsmod  16267  lgsdir2  16274  lgsdirprm  16275  lgsdilem2  16277  lgsdi  16278  lgsne0  16279  lgssq2  16282  lgsdirnn0  16288  lgsdinn0  16289  gausslemma2dlem1a  16299  gausslemma2dlem1f1o  16301  gausslemma2dlem2  16303  gausslemma2dlem3  16304  gausslemma2dlem4  16305  gausslemma2dlem5  16307  gausslemma2dlem6  16308  gausslemma2d  16310  lgseisenlem1  16311  lgseisenlem2  16312  lgseisenlem3  16313  lgseisenlem4  16314  lgsquadlem1  16318  lgsquadlem2  16319  lgsquadlem3  16320  lgsquad2lem1  16322  lgsquad2lem2  16323  lgsquad2  16324  lgsquad3  16325  m1lgs  16326  2lgslem3c  16336  2lgslem3d  16337  2lgslem3d1  16341  2sqlem2  16356  2sqlem3  16358  2sqlem4  16359  2sqlem8  16364  2sqlem9  16365  2sqlem10  16366  vtxdumgrfival  16661  p1evtxdeqfi  16675  p1evtxdp1fi  16676  iswlk  16686  upgr2wlkdc  16740  wlkres  16742  trlreslem  16752  isclwwlk  16757  clwwlkccatlem  16763  clwwlknp  16780  clwwlkn1  16781  clwwlkn2  16784  clwwlkext2edg  16785  clwwlknonex2lem1  16800  clwwlknonex2lem2  16801  clwwlknonex2  16802  iseupth  16810  eupth2lem3lem6fi  16834  eupth2lem3lem4fi  16836  depindlem1  16869  qdencn  17194  trilpolemclim  17207  trilpolemcl  17208  trilpolemisumle  17209  trilpolemeq1  17211  trilpolemlt1  17212  trilpo  17214  apdifflemf  17217  apdiff  17219  iswomni0  17223  redcwlpolemeq1  17226  redcwlpo  17227  nconstwlpolem0  17235  nconstwlpolemgt0  17236  nconstwlpo  17238  neapmkv  17240