Theorem oveq1i 7400

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

Hypothesis

Ref	Expression
oveq1i.1	⊢ 𝐴 = 𝐵

Assertion

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

Proof of Theorem oveq1i

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

Syntax hints:   = wceq 1540  (class class class)co 7390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393

This theorem is referenced by:  caov12  7620  caov411  7624  omopthlem1  8626  map1  9014  pw2eng  9052  fsuppunbi  9347  cnfcomlem  9659  cnfcom2  9662  infxpenc2  9982  adderpqlem  10914  addassnq  10918  distrnq  10921  halfnq  10936  archnq  10940  addclprlem2  10977  addcmpblnr  11029  ltsrpr  11037  m1m1sr  11053  recexsrlem  11063  sqgt0sr  11066  map2psrpr  11070  axi2m1  11119  axcnre  11124  mul02lem2  11358  addrid  11361  cnegex2  11363  addlid  11364  mvrraddi  11445  mvrladdi  11446  mvlladdi  11447  negsubdi  11485  mulneg1  11621  recextlem1  11815  recdiv  11895  divmul13i  11950  mvllmuli  12022  2p2e4  12323  2times  12324  1p2e3  12331  3p2e5  12339  3p3e6  12340  4p2e6  12341  4p3e7  12342  4p4e8  12343  5p2e7  12344  5p3e8  12345  5p4e9  12346  6p2e8  12347  6p3e9  12348  7p2e9  12349  8th4div3  12409  halfpm6th  12411  nneo  12625  9p1e10  12658  dfdec10  12659  num0h  12668  numsuc  12670  dec10p  12699  numma  12700  nummac  12701  numma2c  12702  numadd  12703  numaddc  12704  nummul2c  12706  decaddci  12717  decsubi  12719  5p5e10  12727  6p4e10  12728  7p3e10  12731  8p2e10  12736  decbin0  12796  decbin2  12797  xmulm1  13248  xadddi2  13264  x2times  13266  elfzp1b  13569  elfzm1b  13570  fz0dif1  13574  fz1ssfz0  13591  fz0to4untppr  13598  fz0to5un2tp  13599  fz0sn0fz1  13613  fz0add1fz1  13703  elfz0lmr  13750  fldiv4p1lem1div2  13804  quoremz  13824  quoremnn0ALT  13826  uzrdgxfr  13939  mulexpz  14074  expaddz  14078  sqrecii  14155  sq4e2t8  14171  cu2  14172  i3  14175  iexpcyc  14179  binom2i  14184  binom3  14196  crreczi  14200  discr  14212  3dec  14238  nn0opthlem1  14240  nn0opth2i  14243  faclbnd  14262  bcp1nk  14289  bcpasc  14293  hashp1i  14375  hashxplem  14405  hashpw  14408  hashfun  14409  hashbc  14425  hash7g  14458  ccatlid  14558  pfxccatin12lem2c  14702  revs1  14737  cats1cat  14834  cats2cat  14835  lsws2  14877  lsws3  14878  lsws4  14879  s3s4  14906  s2s5  14907  s5s2  14908  imre  15081  crim  15088  remullem  15101  cnpart  15213  sqrtneglem  15239  absexpz  15278  absimle  15282  sqreulem  15333  amgm2  15343  iseraltlem2  15656  iseraltlem3  15657  modfsummod  15767  binomlem  15802  binom11  15805  arisum  15833  arisum2  15834  pwdif  15841  georeclim  15845  geo2sum  15846  mertenslem1  15857  mertens  15859  prodfrec  15868  fprodm1s  15943  fprodp1s  15944  fprodmodd  15970  fallfacfwd  16009  0risefac  16011  bpolydiflem  16027  bpoly2  16030  bpoly3  16031  bpoly4  16032  fsumcube  16033  efzval  16077  resinval  16110  recosval  16111  efi4p  16112  tan0  16126  efival  16127  sinhval  16129  coshval  16130  cosadd  16140  cos2tsin  16154  ef01bndlem  16159  cos1bnd  16162  cos2bnd  16163  absefib  16173  efieq1re  16174  demoivreALT  16176  eirrlem  16179  rpnnen2lem3  16191  rpnnen2lem11  16199  ruclem7  16211  3dvds  16308  3dvdsdec  16309  3dvds2dec  16310  odd2np1  16318  nn0o1gt2  16358  nn0o  16360  pwp1fsum  16368  divalglem2  16372  divalglem9  16378  5ndvds3  16390  5ndvds6  16391  flodddiv4  16392  m1bits  16417  sadcp1  16432  sadeq  16449  smupp1  16457  smumul  16470  gcdaddmlem  16501  nn0expgcd  16541  3lcm2e6woprm  16592  nn0gcdsq  16729  phiprmpw  16753  prmdiv  16762  prmdiveq  16763  pythagtriplem1  16794  pythagtriplem12  16804  pythagtriplem14  16806  pockthi  16885  infpnlem1  16888  prmreclem4  16897  4sqlem12  16934  4sqlem13  16935  4sqlem19  16941  vdwapun  16952  vdwlem6  16964  0hashbc  16985  prmo2  17018  prmo3  17019  dec5dvds  17042  dec5nprm  17044  dec2nprm  17045  modxai  17046  modxp1i  17048  mod2xnegi  17049  modsubi  17050  gcdmodi  17052  decsplit0b  17057  decsplit1  17059  decsplit  17060  karatsuba  17061  2exp7  17065  2exp8  17066  3exp3  17069  5prm  17086  7prm  17088  11prm  17092  prmlem2  17097  37prm  17098  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  prmo5  17106  1259lem1  17108  1259lem2  17109  1259lem3  17110  1259lem4  17111  1259lem5  17112  2503lem1  17114  2503lem2  17115  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  pwsbas  17457  rcaninv  17763  subsubc  17822  xpccatid  18156  subsubmgm  18644  subsubm  18750  smndex2dnrinv  18849  mulg2  19022  subsubg  19088  oppgmnd  19293  gsumwrev  19305  psgnunilem2  19432  sylow1lem1  19535  subgslw  19553  sylow3  19570  efginvrel2  19664  efgsfo  19676  frgpnabllem1  19810  gsumzaddlem  19858  gsummptfzsplitl  19870  gsummpt1n0  19902  dprdfid  19956  ablfac1lem  20007  pgpfac1lem3  20016  pgpfaclem1  20020  ablsimpgfindlem1  20046  mgpress  20066  srgbinomlem4  20145  opprrng  20261  unitsubm  20302  subsubrng  20479  subsubrg  20514  cntzsdrg  20718  subdrgint  20719  lsslss  20874  xrsnsgrp  21326  gzrngunit  21357  expghm  21392  pzriprng1ALT  21413  chrid  21442  zrhpsgnmhm  21500  psgndiflemA  21517  frlmip  21694  frlmphl  21697  evlsval  22000  mpff  22018  coe1fzgsumdlem  22197  evl1gsumdlem  22250  matvsca2  22322  mattposvs  22349  m2detleiblem3  22523  m2detleiblem4  22524  cpmidpmat  22767  resstopn  23080  cnmpt1res  23570  ressuss  24157  iscusp2  24196  ucnextcn  24198  txmetcnp  24442  rerest  24699  xrtgioo  24702  xrrest  24703  cnmpopc  24829  xrhmeo  24851  clmvs2  25001  clmnegneg  25011  ncvsm1  25061  ncvspi  25063  cphassir  25122  cphipval2  25148  reust  25288  rrxprds  25296  csbren  25306  rrxdsfi  25318  minveclem2  25333  ovolunlem1a  25404  ovolicc2lem4  25428  uniioombllem5  25495  iblabs  25737  iblabsr  25738  iblmulc2  25739  itgmulc2  25742  limcres  25794  dvfval  25805  dvreslem  25817  dvres2lem  25818  dvcnp2  25828  dvcnp2OLD  25829  cpnres  25846  dvmulbr  25848  dvcobr  25856  dvcobrOLD  25857  dveflem  25890  lhop1lem  25925  lhop2  25927  dvcnvrelem2  25930  plyun0  26109  coeeulem  26136  coeeu  26137  dvply1  26198  dvtaylp  26285  taylthlem2  26289  taylthlem2OLD  26290  taylth  26291  dvradcnv  26337  pserdvlem2  26345  abelthlem8  26356  abelth  26358  sinhalfpilem  26379  cospi  26388  eulerid  26390  cos2pi  26392  ef2kpi  26394  sinhalfpip  26408  sinhalfpim  26409  coshalfpip  26410  coshalfpim  26411  sincosq3sgn  26416  sincosq4sgn  26417  tangtx  26421  sincos4thpi  26429  sincos6thpi  26432  sineq0  26440  tanregt0  26455  logm1  26505  abslogle  26534  tanarg  26535  logcnlem4  26561  advlogexp  26571  cxpsqrt  26619  dvsqrt  26658  dvcnsqrt  26660  cxpcn3  26665  root1cj  26673  cxpeq  26674  logb1  26686  2logb9irr  26712  sqrt2cxp2logb9e3  26716  ang180lem1  26726  ang180lem2  26727  ang180lem3  26728  lawcos  26733  isosctrlem1  26735  isosctrlem2  26736  quad2  26756  1cubrlem  26758  1cubr  26759  dcubic2  26761  mcubic  26764  binom4  26767  dquartlem1  26768  quart1lem  26772  quart1  26773  quartlem1  26774  asinlem  26785  asinlem2  26786  asinlem3a  26787  acosneg  26804  efiasin  26805  asinsinlem  26808  asinsin  26809  acoscos  26810  asin1  26811  acosbnd  26817  atancj  26827  efiatan  26829  atanlogaddlem  26830  efiatan2  26834  2efiatan  26835  tanatan  26836  cosatan  26838  atantan  26840  atanbndlem  26842  atans2  26848  dvatan  26852  atantayl  26854  atantayl2  26855  log2cnv  26861  log2tlbnd  26862  log2ublem2  26864  log2ublem3  26865  log2ub  26866  birthday  26871  jensenlem1  26904  amgmlem  26907  lgamgulmlem2  26947  lgamgulmlem5  26950  lgambdd  26954  ftalem2  26991  ftalem5  26994  ftalem6  26995  basellem2  26999  basellem3  27000  basellem5  27002  basellem8  27005  basellem9  27006  mule1  27065  ppi1i  27085  musum  27108  ppiublem1  27120  ppiub  27122  chtublem  27129  chtub  27130  dchrptlem1  27182  dchrptlem2  27183  bclbnd  27198  bposlem6  27207  bposlem8  27209  bposlem9  27210  lgsdir2lem1  27243  lgsdir2lem2  27244  lgsdir2lem4  27246  lgsdir2lem5  27247  lgsne0  27253  1lgs  27258  gausslemma2dlem0e  27278  gausslemma2dlem0f  27279  gausslemma2dlem3  27286  gausslemma2d  27292  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgseisenlem4  27296  lgseisen  27297  lgsquadlem1  27298  lgsquadlem2  27299  lgsquad2lem1  27302  lgsquad2lem2  27303  m1lgs  27306  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2lgsoddprmlem3a  27328  2lgsoddprmlem3b  27329  2lgsoddprmlem3c  27330  2lgsoddprmlem3d  27331  addsqnreup  27361  chebbnd1lem2  27388  chebbnd1lem3  27389  rplogsumlem2  27403  dchrisum0flblem1  27426  dchrisum0re  27431  mulog2sumlem2  27453  chpdifbndlem1  27471  pntpbnd1a  27503  pntpbnd2  27505  pntibndlem2  27509  pntibndlem3  27510  pntlemg  27516  pntlemk  27524  pntlemo  27525  no2times  28310  zseo  28315  remulscllem1  28358  axsegconlem1  28851  ax5seglem7  28869  axlowdimlem3  28878  axlowdimlem16  28891  axlowdimlem17  28892  elntg2  28919  vdegp1bi  29472  vtxdginducedm1  29478  wlkp1lem1  29608  spthispth  29661  cyclnumvtx  29737  2wlkdlem1  29862  2pthd  29877  clwlkclwwlkfo  29945  3wlkdlem1  30095  3pthd  30110  eucrct2eupth  30181  numclwwlk5  30324  numclwwlk7  30327  frgrregord013  30331  ex-fl  30383  ex-mod  30385  ex-exp  30386  ex-bc  30388  ex-lcm  30394  ex-ind-dvds  30397  vc2OLD  30504  vc0  30510  vcm  30512  nvm1  30601  nvpi  30603  nvmtri  30607  nvge0  30609  ipval3  30645  ipidsq  30646  ip0i  30761  ip1ilem  30762  ip2i  30764  ipdirilem  30765  ipasslem10  30775  siilem1  30787  siii  30789  minvecolem2  30811  hvsubid  30962  hvaddsubval  30969  hvmul2negi  30984  hvadd12i  30993  hv2times  30997  hvnegdii  30998  hvaddcani  31001  hi01  31032  hisubcomi  31040  normlem0  31045  normlem1  31046  normlem3  31048  normlem9  31054  bcseqi  31056  normsqi  31068  norm-ii-i  31073  normsubi  31077  norm3difi  31083  norm3adifii  31084  normpar2i  31092  polid2i  31093  polidi  31094  chdmm2i  31414  chj12i  31458  spanunsni  31515  qlaxr5i  31571  osumcor2i  31580  spansnji  31582  pjadjii  31610  pjinormii  31612  pjsslem  31615  pjpythi  31658  mayete3i  31664  mayetes3i  31665  hoadd12i  31713  honegneg  31742  ho2times  31755  hoaddsubi  31757  hosd1i  31758  hosd2i  31759  honpncani  31763  lnopeq0lem1  31941  lnopunilem1  31946  lnophmlem2  31953  lnfn0i  31978  nmopcoadji  32037  nmopcoadj2i  32038  opsqrlem1  32076  opsqrlem5  32080  opsqrlem6  32081  pjclem3  32133  stadd3i  32184  mddmd2  32245  mdexchi  32271  cvexchlem  32304  atomli  32318  atordi  32320  atabs2i  32338  mdsymlem1  32339  iuninc  32496  suppss2f  32569  mptiffisupp  32623  suppss3  32654  binom2subadd  32672  pythagreim  32676  dfdec100  32762  dpfrac1  32819  decdiv10  32823  dpmul100  32824  dp3mul10  32825  dpmul1000  32826  dpexpp1  32835  dpadd2  32837  dpadd  32838  dpmul  32840  dpmul4  32841  threehalves  32842  1mhdrd  32843  pfxlsw2ccat  32879  ccatws1f1olast  32881  chnub  32945  cyc2fv1  33085  cyc2fv2  33086  cycpmco2lem4  33093  cycpmco2lem5  33094  cyc3fv1  33101  cyc3fv2  33102  cyc3fv3  33103  archirngz  33150  gsumvsca2  33187  elrgspnlem4  33203  subsdrg  33255  nn0omnd  33323  nn0archi  33325  xrge0slmod  33326  opprabs  33460  ressply1evls1  33541  resssra  33590  lsssra  33591  fedgmullem1  33632  fedgmullem2  33633  fedgmul  33634  fldsdrgfldext2  33665  fldgenfldext  33670  fldextrspunlem1  33677  fldextrspunfld  33678  fldextrspundgdvdslem  33682  fldextrspundgdvds  33683  algextdeglem1  33714  algextdeglem4  33717  constrrtcclem  33731  constrmulcl  33768  constrinvcl  33770  2sqr3minply  33777  cos9thpiminplylem4  33782  cos9thpiminplylem5  33783  lmatfvlem  33812  sqsscirc1  33905  cnvordtrestixx  33910  raddcn  33926  xrge0iifhom  33934  xrge0mulc1cn  33938  xrge0tmd  33942  lmlimxrge0  33945  qqhucn  33989  rrhcn  33994  qqtopn  34008  rrhqima  34011  brfae  34245  inelcarsg  34309  cndprobnul  34435  isrrvv  34441  ballotlem1  34485  ballotlem2  34487  ballotlemi1  34501  ballotlemii  34502  ballotlemic  34505  ballotlem1c  34506  ballotlemfrceq  34527  ballotth  34536  ofcs2  34543  signsvtn0  34568  signstfveq0  34575  signsvtp  34581  signsvtn  34582  signsvfpn  34583  signsvfnn  34584  signshf  34586  hashreprin  34618  reprfz1  34622  chtvalz  34627  breprexp  34631  breprexpnat  34632  hgt750lemd  34646  hgt750lem  34649  hgt750lem2  34650  subfacp1lem1  35173  subfacp1lem5  35178  subfacp1lem6  35179  subfaclim  35182  cvmliftlem5  35283  cvmliftlem8  35286  cvmliftlem10  35288  cvmliftlem13  35290  cvmlift2lem6  35302  cvmlift2lem12  35308  problem1  35659  problem2  35660  problem4  35662  quad3  35664  iexpire  35729  itgeq12i  36201  sin2h  37611  poimirlem16  37637  poimirlem17  37638  poimirlem18  37639  poimirlem19  37640  poimirlem20  37641  poimirlem21  37642  poimirlem22  37643  poimirlem26  37647  mblfinlem3  37660  ismblfin  37662  itg2addnclem3  37674  iblabsnc  37685  iblmulc2nc  37686  itgmulc2nc  37689  ftc1cnnc  37693  ftc1anclem6  37699  ftc1anclem7  37700  ftc1anclem8  37701  dvasin  37705  fdc  37746  heiborlem4  37815  heiborlem6  37817  dalem24  39698  pmod2iN  39850  cdleme9  40254  cdleme20aN  40310  cdleme22e  40345  cdleme22eALTN  40346  cdleme25cv  40359  cdleme29b  40376  cdlemh1  40816  cdlemh2  40817  cdlemk35  40913  cdlemkid1  40923  12gcd5e1  41998  60gcd7e1  42000  420gcd8e4  42001  12lcm5e60  42003  420lcm8e840  42006  lcm1un  42008  lcm2un  42009  lcm3un  42010  lcm4un  42011  lcm5un  42012  lcm6un  42013  lcm7un  42014  lcm8un  42015  3factsumint1  42016  3factsumint3  42018  lcmineqlem10  42033  3exp7  42048  3lexlogpow5ineq1  42049  3lexlogpow5ineq5  42055  aks4d1p1  42071  5bc2eq10  42137  2ap1caineq  42140  aks5lem3a  42184  aks5lem7  42195  1p3e4  42254  sqmid3api  42278  sqn5i  42280  sqdeccom12  42284  235t711  42300  cxpi11d  42338  sin2t3rdpi  42348  cos2t3rdpi  42349  re1m1e0m0  42392  readdlid  42398  remul02  42400  sn-1ticom  42430  sn-mullid  42431  sn-0tie0  42446  sn-mul02  42447  sn-inelr  42482  mhphf2  42593  flt4lem5e  42651  sum9cubes  42667  pellexlem5  42828  reglog1  42891  jm2.23  42992  jm2.27c  43003  lnmlsslnm  43077  lmhmlnmsplit  43083  areaquad  43212  oaomoencom  43313  resqrtvalex  43641  imsqrtvalex  43642  cotrclrcl  43738  inductionexd  44151  hashnzfz2  44317  lhe4.4ex1a  44325  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  binomcxp  44353  sineq0ALT  44933  unirnmapsn  45215  fzisoeu  45305  fsummulc1f  45576  fprodexp  45599  constlimc  45629  sumnnodd  45635  limcresiooub  45647  limcresioolb  45648  cncfshiftioo  45897  fperdvper  45924  dvnmul  45948  dvmptfprod  45950  itgsinexplem1  45959  stoweidlem11  46016  stoweidlem13  46018  stoweidlem26  46031  stoweidlem34  46039  wallispilem4  46073  wallispi2lem1  46076  wallispi2lem2  46077  stirlinglem11  46089  dirkerper  46101  dirkertrigeqlem1  46103  dirkertrigeqlem3  46105  dirkercncflem1  46108  dirkercncflem4  46111  fourierdlem30  46142  fourierdlem32  46144  fourierdlem33  46145  fourierdlem42  46154  fourierdlem46  46157  fourierdlem47  46158  fourierdlem57  46168  fourierdlem60  46171  fourierdlem61  46172  fourierdlem62  46173  fourierdlem68  46179  fourierdlem73  46184  fourierdlem79  46190  fourierdlem89  46200  fourierdlem90  46201  fourierdlem91  46202  fourierdlem96  46207  fourierdlem97  46208  fourierdlem98  46209  fourierdlem99  46210  fourierdlem100  46211  fourierdlem103  46214  fourierdlem104  46215  fourierdlem108  46219  fourierdlem110  46221  fourierdlem113  46224  sqwvfoura  46233  sqwvfourb  46234  fourierswlem  46235  fouriersw  46236  fouriercn  46237  etransclem4  46243  etransclem7  46246  etransclem23  46262  etransclem24  46263  etransclem25  46264  etransclem26  46265  etransclem31  46270  etransclem32  46271  etransclem35  46274  etransclem37  46276  etransclem46  46285  rrndistlt  46295  sge0tsms  46385  sge0xaddlem2  46439  vonioolem2  46686  ormklocald  46879  natlocalincr  46881  upwordsing  46889  tworepnotupword  46891  1t10e1p1e11  47315  deccarry  47316  1fzopredsuc  47329  ceil5half3  47345  minusmodnep2tmod  47358  m1mod0mod1  47359  8mod5e3  47365  modmkpkne  47366  modm1p1ne  47375  iccpartgt  47432  fmtno0  47545  fmtno1  47546  fmtnorec2  47548  fmtno2  47555  fmtno3  47556  fmtno4  47557  fmtno5  47562  257prm  47566  fmtnofac1  47575  fmtno4prmfac  47577  fmtno4prmfac193  47578  fmtno4nprmfac193  47579  m2prm  47596  m3prm  47597  flsqrt5  47599  3ndvds4  47600  139prmALT  47601  31prm  47602  127prm  47604  m11nprm  47606  lighneallem2  47611  lighneallem3  47612  3exp4mod41  47621  41prothprmlem1  47622  41prothprmlem2  47623  41prothprm  47624  m1expevenALTV  47652  1oddALTV  47695  6even  47716  8even  47718  2exp340mod341  47738  341fppr2  47739  4fppr1  47740  8exp8mod9  47741  9fppr8  47742  nfermltl8rev  47747  gbpart7  47772  gbpart9  47774  gbpart11  47775  sbgoldbo  47792  bgoldbtbndlem1  47810  tgoldbachlt  47821  gpg3kgrtriexlem2  48079  gpg3kgrtriexlem4  48081  gpg3kgrtriexlem6  48083  gpg3kgrtriex  48084  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem11  48099  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  altgsumbcALT  48345  lincfsuppcl  48406  linccl  48407  lincvalsn  48410  lincdifsn  48417  lincsum  48422  lincscm  48423  lindslinindimp2lem4  48454  lindslinindsimp2lem5  48455  snlindsntor  48464  lincresunit3lem2  48473  zlmodzxzldeplem3  48495  ldepsnlinc  48501  nn0sumshdiglemA  48612  nn0sumshdiglemB  48613  ackval2  48675  ackval2012  48684  ackval3012  48685  ackval41a  48687  ackval42  48689  ackval42a  48690  affinecomb1  48695  rrx2linest  48735  itschlc0yqe  48753  itsclc0yqsollem1  48755  itscnhlc0xyqsol  48758  itschlc0xyqsol1  48759  itsclquadb  48769  2itscplem2  48772  itscnhlinecirc02plem2  48776  oppcup  49200  natoppf  49222  islmd  49658  iscmd  49659  lmddu  49660  sinh-conventional  49732  onetansqsecsq  49754  cotsqcscsq  49755  mvlraddi  49764  mvlrmuli  49770  amgmwlem  49795  amgmlemALT  49796