Theorem oveq2i 7167

Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.)

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
oveq2i	⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Proof of Theorem oveq2i

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 ⊢ 𝐴 = 𝐵
2		oveq2 7164	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐶𝐹𝐴) = (𝐶𝐹𝐵)

Syntax hints:   = wceq 1537  (class class class)co 7156

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363  df-ov 7159

This theorem is referenced by:  caov32  7375  caov4  7379  caov42  7381  seqomsuc  8093  oa1suc  8156  o2p2e4  8166  o2p2e4OLD  8167  om1  8168  oe1  8170  oawordeulem  8180  oeoalem  8222  nnm1  8275  nnm2  8276  nneob  8279  omopthlem1  8282  mapsnconst  8456  mapsncnv  8457  map2xp  8687  cantnflt  9135  cnfcom2  9165  infxpenc  9444  infxpenc2  9448  mapdjuen  9606  ackbij1lem5  9646  alephom  10007  pwxpndom2  10087  adderpqlem  10376  addassnq  10380  mulcanenq  10382  distrnq  10383  ltanq  10393  ltexnq  10397  halfnq  10398  ltrnq  10401  archnq  10402  addclprlem2  10439  prlem934  10455  prlem936  10469  addcmpblnr  10491  mulcmpblnrlem  10492  ltsrpr  10499  m1p1sr  10514  m1m1sr  10515  0idsr  10519  1idsr  10520  00sr  10521  pn0sr  10523  recexsrlem  10525  mulgt0sr  10527  sqgt0sr  10528  mulresr  10561  axmulcom  10577  axmulass  10579  axdistr  10580  axi2m1  10581  ax1rid  10583  axcnre  10586  mul02lem1  10816  addid1  10820  negid  10933  negsub  10934  subneg  10935  negsubdii  10971  muleqadd  11284  crne0  11631  2p2e4  11773  1p2e3  11781  3p2e5  11789  3p3e6  11790  4p2e6  11791  4p3e7  11792  4p4e8  11793  5p2e7  11794  5p3e8  11795  5p4e9  11796  6p2e8  11797  6p3e9  11798  7p2e9  11799  3t3e9  11805  8th4div3  11858  halfpm6th  11859  addltmul  11874  div4p1lem1div2  11893  nn0n0n1ge2  11963  nneo  12067  zeo  12069  numsuc  12113  numltc  12125  numsucc  12139  numma  12143  nummul1c  12148  decrmac  12157  decsubi  12162  decmul10add  12168  6p5lem  12169  5p5e10  12170  6p4e10  12171  7p3e10  12174  8p2e10  12179  4t3lem  12196  9t11e99  12229  decbin2  12240  xmulmnf1  12670  fztp  12964  fz12pr  12965  fztpval  12970  fzshftral  12996  fz0tp  13009  fz0to3un2pr  13010  fzo01  13120  fzo12sn  13121  fzo13pr  13122  fzo0to2pr  13123  fzo0to3tp  13124  fzo0to42pr  13125  fzo1to4tp  13126  fzosplitprm1  13148  quoremz  13224  quoremnn0ALT  13226  intfrac2  13227  intfracq  13228  sqval  13482  sqrecii  13547  sq4e2t8  13563  cu2  13564  i3  13567  i4  13568  binom2i  13575  binom3  13586  crreczi  13590  3dec  13627  nn0opthlem1  13629  facp1  13639  faclbnd  13651  faclbnd2  13652  faclbnd4lem1  13654  faclbnd4lem4  13657  bcn1  13674  bcn2  13680  4bc3eq4  13689  4bc2eq6  13690  hashgadd  13739  hashxplem  13795  hashmap  13797  hashfun  13799  hashbclem  13811  fz1isolem  13820  ccatlid  13940  ccatrid  13941  ccatws1len  13974  ccats1val2  13983  ccat2s1p2  13986  ccat2s1p2OLD  13988  pfx1  14065  pfxccatin12lem3  14094  pfxccatpfx1  14098  pfxccatpfx2  14099  cats1fvn  14220  cats1cat  14223  cats2cat  14224  s3fn  14273  swrds2  14302  swrds2m  14303  reim0  14477  cji  14518  sqrtm1  14635  absi  14646  rddif  14700  iseraltlem2  15039  iseralt  15041  fsump1i  15124  fsummulc2  15139  incexclem  15191  incexc  15192  arisum2  15216  geoihalfsum  15238  mertenslem1  15240  mertens  15242  risefall0lem  15380  risefac1  15387  fallfac1  15388  fallfacfwd  15390  bpoly0  15404  bpoly1  15405  bpolydiflem  15408  bpoly2  15411  bpoly3  15412  bpoly4  15413  fsumcube  15414  ef0lem  15432  ege2le3  15443  eft0val  15465  ef4p  15466  efgt1p2  15467  efgt1p  15468  tanval2  15486  efival  15505  ef01bndlem  15537  sin01bnd  15538  cos01bnd  15539  cos1bnd  15540  cos2bnd  15541  rpnnen2lem11  15577  3dvdsdec  15681  3dvds2dec  15682  odd2np1lem  15689  odd2np1  15690  oddp1even  15693  opoe  15712  divalglem5  15748  divalglem6  15749  bits0  15777  0bits  15788  gcdaddmlem  15872  6gcd4e2  15886  lcmneg  15947  3lcm2e6woprm  15959  6lcm4e12  15960  3prm  16038  3lcm2e6  16072  phiprm  16114  eulerthlem2  16119  prmdiv  16122  pythagtriplem12  16163  pythagtriplem14  16165  pcmpt  16228  pcfac  16235  prmpwdvds  16240  pockthi  16243  prmreclem2  16253  prmreclem6  16257  4sqlem5  16278  4sqlem13  16293  modxai  16404  mod2xnegi  16407  gcdi  16409  decexp2  16411  numexpp1  16414  numexp2x  16415  decsplit0b  16416  decsplit1  16418  decsplit  16419  2exp16  16424  prmlem0  16439  139prm  16457  163prm  16458  317prm  16459  631prm  16460  1259lem4  16467  1259lem5  16468  1259prm  16469  2503lem1  16470  2503lem2  16471  2503lem3  16472  2503prm  16473  4001lem1  16474  4001lem4  16477  ressinbas  16560  rcaninv  17064  rescfth  17207  xpccatid  17438  oduval  17740  oppgmnd  18482  psgnunilem2  18623  psgnunilem4  18625  psgnpmtr  18638  psgn0fv0  18639  psgnsn  18648  psgnprfval1  18650  lsmmod2  18802  efgi0  18846  efgi1  18847  efginvrel2  18853  efgsval2  18859  efgsp1  18863  efgredleme  18869  efgredlemc  18871  efgcpbllemb  18881  frgpnabllem1  18993  lt6abl  19015  gsumconstf  19055  gsum2dlem2  19091  pwsgsum  19102  fsfnn0gsumfsffz  19103  dprd0  19153  dprdf1  19155  dprd2da  19164  ablfac1lem  19190  pgpfac1lem3  19199  pgpfaclem1  19203  srgbinomlem4  19293  opprring  19381  mulgass3  19387  evlsval  20299  mpff  20317  ply1assa  20367  gsumply1subr  20402  ply1coe  20464  coe1fzgsumdlem  20469  coe1fzgsumd  20470  gsumply1eq  20473  evl1gsumdlem  20519  evl1gsumd  20520  xrsnsgrp  20581  znbas  20690  znzrh2  20692  dsmmval2  20880  frlmip  20922  matgsum  21046  madetsumid  21070  mdetrsca  21212  mdetrsca2  21213  mdettpos  21220  m2detleiblem2  21237  madugsum  21252  madurid  21253  cpmat  21317  pmatcollpwfi  21390  pmatcollpw3fi1lem1  21394  pm2mpval  21403  mp2pm2mplem5  21418  chpmat1dlem  21443  chpmat1d  21444  chpidmat  21455  cpmidpmat  21481  cpmadugsumfi  21485  chcoeffeqlem  21493  cayleyhamilton0  21497  cayleyhamiltonALT  21499  cayleyhamilton1  21500  restin  21774  imacmp  22005  conncompconn  22040  uptx  22233  cnpflf2  22608  tmdgsum2  22704  tsmsres  22752  tsmsf1o  22753  tsmsmhm  22754  prdsxmet  22979  resspwsds  22982  prdsxmslem2  23139  tngngpim  23268  metdcn2  23447  metdcn  23448  metdscn2  23465  iimulcn  23542  icchmeo  23545  xrhmeo  23550  cnrehmeo  23557  cnheiborlem  23558  evth  23563  evth2  23564  lebnumlem2  23566  reparphti  23601  pcoass  23628  pi1xfrcnv  23661  ipcau2  23837  ehl0base  24019  minveclem4  24035  pjthlem1  24040  ovolunlem1a  24097  unmbl  24138  uniioombl  24190  iblitg  24369  dfitg  24370  itg0  24380  iblcnlem1  24388  itgcnlem  24390  itgabs  24435  limcdif  24474  limccnp  24489  limccnp2  24490  dvexp  24550  dvmptid  24554  dvmptc  24555  dvmptfsum  24572  dveflem  24576  dvsincos  24578  mvth  24589  dvlipcn  24591  dvivthlem1  24605  dvfsumle  24618  dvfsumlem2  24624  itgsubst  24646  tdeglem4  24654  tdeglem2  24655  plypf1  24802  plymullem1  24804  coesub  24847  dgrmulc  24861  fta1lem  24896  vieta1lem1  24899  vieta1lem2  24900  aalioulem4  24924  aaliou3lem3  24933  abelthlem2  25020  abelthlem8  25027  abelthlem9  25028  sinhalfpilem  25049  efhalfpi  25057  cospi  25058  efipi  25059  sin2pi  25061  cos2pi  25062  ef2pi  25063  sin2pim  25071  cos2pim  25072  sinmpi  25073  cosmpi  25074  sinppi  25075  cosppi  25076  sincosq4sgn  25087  tangtx  25091  sincos4thpi  25099  sincos6thpi  25101  sincos3rdpi  25102  pige3ALT  25105  abssinper  25106  efif1olem4  25129  efifo  25131  eff1o  25133  circgrp  25136  circsubm  25137  logneg  25171  logimul  25197  logneg2  25198  dvrelog  25220  logcnlem4  25228  dvlog  25234  dvlog2  25236  logtayl  25243  1cxp  25255  ecxp  25256  cxpsqrt  25286  2irrexpq  25313  dvsqrt  25323  dvcnsqrt  25325  root1eq1  25336  cxpeq  25338  elogb  25348  2logb9irrALT  25376  ang180lem1  25387  ang180lem2  25388  heron  25416  1cubrlem  25419  1cubr  25420  dcubic2  25422  mcubic  25425  cubic2  25426  binom4  25428  dquartlem1  25429  dquartlem2  25430  dquart  25431  quart1lem  25433  quart1  25434  quartlem1  25435  asinsin  25470  asin1  25472  acos1  25473  atanlogsublem  25493  atanlogsub  25494  efiatan2  25495  2efiatan  25496  tanatan  25497  atanbnd  25504  atan1  25506  dvatan  25513  atantayl2  25516  leibpilem2  25519  leibpi  25520  log2cnv  25522  log2tlbnd  25523  log2ublem1  25524  log2ublem2  25525  log2ublem3  25526  log2ub  25527  birthday  25532  amgmlem  25567  emcllem5  25577  lgamgulmlem2  25607  lgamgulmlem5  25610  lgam1  25641  wilthlem2  25646  ftalem6  25655  basellem2  25659  basellem3  25660  basellem5  25662  basellem8  25665  cht1  25742  chp1  25744  1sgmprm  25775  ppiublem2  25779  ppiub  25780  chtublem  25787  chtub  25788  logfacbnd3  25799  bcp1ctr  25855  bclbnd  25856  bposlem4  25863  bposlem6  25865  bposlem8  25867  bposlem9  25868  lgslem1  25873  lgsdir2lem1  25901  lgsdir2lem2  25902  lgsdir2lem3  25903  lgsdir2lem5  25905  lgs1  25917  gausslemma2dlem1a  25941  gausslemma2dlem3  25944  gausslemma2dlem4  25945  gausslemma2d  25950  lgseisenlem1  25951  lgseisenlem3  25953  lgsquadlem1  25956  lgsquadlem2  25957  lgsquad2lem2  25961  m1lgs  25964  2lgslem1a2  25966  2sqlem8  26002  2sqblem  26007  addsq2nreurex  26020  logdivsum  26109  mulog2sumlem2  26111  log2sumbnd  26120  selberglem1  26121  selberglem2  26122  pntrmax  26140  pntibndlem2  26167  pntibndlem3  26168  pntlemg  26174  pntlemr  26178  pntlemo  26183  ostth2lem3  26211  ostth2lem4  26212  istrkg3ld  26247  trgcgrg  26301  tgcgr4  26317  colperpexlem1  26516  ax5seglem7  26721  axlowdimlem16  26743  setsiedg  26821  vdegp1ci  27320  finsumvtxdg2sstep  27331  finsumvtxdg2size  27332  wlkp1lem6  27460  wlkp1lem8  27462  wlkp1  27463  uhgrwkspthlem2  27535  pthdlem1  27547  pthdlem2  27549  pthd  27550  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  crctcshwlkn0lem6  27593  crctcshlem4  27598  crctcshwlkn0  27599  2wlkdlem2  27705  2wlkdlem4  27707  2pthdlem1  27709  wwlks2onv  27732  clwlkclwwlk2  27781  clwwlkwwlksb  27833  wwlksext2clwwlk  27836  clwwlknonex2lem1  27886  0ewlk  27893  1ewlk  27894  0wlk  27895  1pthdlem1  27914  1pthdlem2  27915  1wlkdlem1  27916  1wlkdlem4  27919  wlk2v2e  27936  3wlkdlem2  27939  3wlkdlem4  27941  3pthdlem1  27943  eupth0  27993  eupthp1  27995  eucrctshift  28022  eucrct2eupth  28024  numclwwlk1lem2foalem  28130  numclwlk2lem2f  28156  frgrregord013  28174  ex-exp  28229  ex-bc  28231  ex-gcd  28236  ex-lcm  28237  ex-ind-dvds  28240  smcnlem  28474  ipidsq  28487  dipcj  28491  dip0r  28494  nmlnoubi  28573  nmblolbii  28576  blocnilem  28581  ip1ilem  28603  ip2i  28605  ipdirilem  28606  ipasslem10  28616  ipasslem11  28617  siilem1  28628  hvmul0  28801  hvsubsub4i  28836  hvnegdii  28839  hvsubeq0i  28840  hvsubcan2i  28841  hvsubaddi  28843  hvsub0  28853  hisubcomi  28881  normlem0  28886  normlem1  28887  normlem2  28888  normlem3  28889  normlem9  28895  norm-ii-i  28914  norm3difi  28924  normpari  28931  polid2i  28934  polidi  28935  bcsiALT  28956  pjhthlem1  29168  chdmm3i  29256  chdmm4i  29257  chjidm  29297  chj4i  29300  chjjdiri  29301  spanunsni  29356  pjoml4i  29364  cmcm2i  29370  qlax4i  29407  qlax5i  29408  pjadjii  29451  pjmulii  29454  pjsubii  29455  pjssmii  29458  pjcji  29461  pjneli  29500  hoadd32i  29555  ho0subi  29572  hosubid1  29575  hosd2i  29600  hopncani  29601  hosubeq0i  29603  lnopeq0lem1  29782  lnopunilem1  29787  lnophmlem2  29794  nmbdoplbi  29801  nmcopexi  29804  lnfnmuli  29821  nmcfnexi  29828  nmoptri2i  29876  nmopcoadji  29878  golem1  30048  mdsl1i  30098  cvmdi  30101  mdslmd3i  30109  csmdsymi  30111  dfdec100  30546  dp20u  30554  dpmul10  30571  dpmul100  30573  dp3mul10  30574  dpmul1000  30575  dpexpp1  30584  0dp2dp  30585  dpmul  30589  dpmul4  30590  1mhdrd  30592  s2rn  30620  s3rn  30622  s3f1  30623  cshw1s2  30634  xrge00  30673  gsummpt2co  30686  gsumle  30725  psgnfzto1st  30747  cyc2fv1  30763  cycpmco2lem5  30772  cycpmco2lem6  30773  cycpmco2  30775  cyc3fv1  30779  cyc3fv2  30780  archirngz  30818  archiabllem2c  30824  gsumvsca1  30854  gsumvsca2  30855  xrge0slmod  30917  fply1  30931  lbsdiflsp0  31022  fedgmul  31027  ccfldextrr  31038  lmat22det  31087  madjusmdetlem4  31095  raddcn  31172  xrge0iifhom  31180  xrge0mulc1cn  31184  cbvesum  31301  gsumesum  31318  esumpfinvallem  31333  esumpfinvalf  31335  dya2icoseg  31535  sitg0  31604  eulerpartlemd  31624  eulerpartlemgvv  31634  eulerpartlemgh  31636  fib0  31657  fib1  31658  fibp1  31659  orrvcval4  31722  orrvcoel  31723  orrvccel  31724  coinflipprob  31737  coinflippvt  31742  ballotlem2  31746  ballotth  31795  signstf0  31838  signstfvn  31839  signsvtn0  31840  signstfvp  31841  signstfveq0  31847  signsvf0  31850  signsvf1  31851  signsvfn  31852  prodfzo03  31874  itgexpif  31877  repr0  31882  hgt750lemd  31919  hgt750lem  31922  hgt750lem2  31923  subfacp1lem1  32426  subfacp1lem5  32431  subfacval2  32434  subfaclim  32435  subfacval3  32436  cvxpconn  32489  cvxsconn  32490  sate0  32662  mrsub0  32763  problem4  32911  quad3  32913  sinccvglem  32915  iexpire  32967  faclimlem1  32975  fprlem1  33137  frrlem15  33142  fwddifnp1  33626  knoppcnlem10  33841  knoppndvlem7  33857  knoppndvlem21  33871  cnndvlem1  33876  finxpreclem4  34678  ptrest  34906  poimirlem27  34934  dvtan  34957  itgabsnc  34976  ftc1anclem8  34989  dvasin  34993  dvacos  34994  areacirclem1  34997  areacirclem4  35000  areacirc  35002  prdstotbnd  35087  prdsbnd2  35088  repwsmet  35127  rrnequiv  35128  reheibor  35132  dalem-cly  36822  pmodN  37001  cdleme0cp  37365  cdleme0cq  37366  cdleme1  37378  cdleme3d  37382  cdleme3h  37386  cdleme4  37389  cdleme5  37391  cdleme7a  37394  cdleme8  37401  cdleme9  37404  cdleme10  37405  cdleme11g  37416  cdleme15b  37426  cdleme21  37488  cdleme22e  37495  cdleme22eALTN  37496  cdleme23c  37502  cdleme25cv  37509  cdleme35b  37601  cdleme35c  37602  cdleme42a  37622  cdleme42d  37624  cdleme43aN  37640  cdlemeg46gfv  37681  cdlemk35  38063  dihjatcclem1  38569  lcdval2  38741  mapdpglem21  38843  gcdaddmzz2nncomi  39122  12gcd5e1  39124  60gcd6e6  39125  60gcd7e1  39126  420gcd8e4  39127  lcmeprodgcdi  39128  420lcm8e840  39132  lcm1un  39134  lcm2un  39135  lcm3un  39136  lcm4un  39137  lcm5un  39138  lcm6un  39139  lcm7un  39140  lcm8un  39141  facp2  39144  sqsumi  39216  sqmid3api  39218  sqn5ii  39221  sq3deccom12  39225  re1m1e0m0  39276  sn-00idlem1  39277  remul02  39284  resubid  39287  mapfzcons  39362  mapfzcons1cl  39364  2rexfrabdioph  39442  3rexfrabdioph  39443  4rexfrabdioph  39444  6rexfrabdioph  39445  7rexfrabdioph  39446  rabdiophlem2  39448  diophren  39459  rabren3dioph  39461  pellexlem5  39479  pell1qr1  39517  rmspecfund  39555  jm2.17a  39606  jm2.17b  39607  jm2.27c  39653  jm2.27dlem5  39659  lmhmlnmsplit  39736  arearect  39871  areaquad  39872  relexp2  40071  trclfvdecomr  40122  k0004val0  40553  inductionexd  40554  unitadd  40597  amgm2d  40600  amgm3d  40601  lhe4.4ex1a  40710  expgrowthi  40714  expgrowth  40716  bccn1  40725  binomcxplemdvbinom  40734  binomcxplemdvsum  40736  binomcxplemnotnn0  40737  binomcxp  40738  refsumcn  41336  unirnmapsn  41526  oddfl  41592  infleinflem2  41688  sumnnodd  41960  cosnegpi  42197  dvcosre  42245  dvsinax  42246  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvmptmulf  42271  dvxpaek  42274  dvmptfprod  42279  dvnprodlem2  42281  dvnprodlem3  42282  itgsin0pilem1  42284  itgsinexplem1  42288  itgsubsticclem  42309  stoweidlem13  42347  wallispilem4  42402  wallispi2lem1  42405  wallispi2lem2  42406  stirlinglem1  42408  dirkerper  42430  dirkertrigeqlem1  42432  dirkertrigeqlem3  42434  dirkertrigeq  42435  dirkeritg  42436  dirkercncflem1  42437  dirkercncflem2  42438  fourierdlem36  42477  fourierdlem41  42482  fourierdlem42  42483  fourierdlem48  42488  fourierdlem56  42496  fourierdlem57  42497  fourierdlem58  42498  fourierdlem60  42500  fourierdlem61  42501  fourierdlem62  42502  fourierdlem65  42505  fourierdlem73  42513  fourierdlem80  42520  fourierdlem87  42527  fourierdlem89  42529  fourierdlem90  42530  fourierdlem91  42531  fourierdlem100  42540  fourierdlem103  42543  fourierdlem107  42547  fourierdlem112  42552  fourierdlem113  42553  fourierdlem115  42555  fouriercnp  42560  sqwvfoura  42562  sqwvfourb  42563  fourierswlem  42564  fouriersw  42565  etransclem2  42570  etransclem37  42605  etransclem46  42614  hoidmvlelem3  42928  vonioolem2  43012  issmflem  43053  smfmullem2  43116  simpcntrab  43176  1t10e1p1e11  43559  fmtno0  43751  fmtno1  43752  fmtnorec2lem  43753  fmtnorec3  43759  fmtno2  43761  fmtno3  43762  fmtno4  43763  fmtno4sqrt  43782  fmtno4prmfac  43783  2exp5  43804  139prmALT  43808  31prm  43809  2exp7  43811  2exp11  43814  mod42tp1mod8  43816  lighneallem2  43820  5tcu2e40  43829  3exp4mod41  43830  41prothprmlem1  43831  41prothprmlem2  43832  41prothprm  43833  bits0ALTV  43893  fppr2odd  43945  341fppr2  43948  4fppr1  43949  9fppr8  43951  sbgoldbo  44001  nnsum3primes4  44002  nnsum3primesgbe  44006  nnsum4primesodd  44010  nnsum4primesoddALTV  44011  nnsum4primeseven  44014  nnsum4primesevenALTV  44015  bgoldbtbndlem1  44019  tgoldbachlt  44030  2t6m3t4e0  44445  zlmodzxzequa  44600  zlmodzxznm  44601  zlmodzxzequap  44603  nn0sumshdiglemA  44728  nn0sumshdiglemB  44729  nn0sumshdiglem1  44730  prelrrx2  44749  prelrrx2b  44750  2sphere  44785  line2  44788  itsclquadb  44812  itscnhlinecirc02plem3  44820  inlinecirc02p  44823  sec0  44908  amgmw2d  44954