Theorem oveq1i 7366

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 7363	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐴𝐹𝐶) = (𝐵𝐹𝐶)

Syntax hints:   = wceq 1541  (class class class)co 7356

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359

This theorem is referenced by:  caov12  7584  caov411  7588  omopthlem1  8585  map1  8975  pw2eng  9009  fsuppunbi  9290  cnfcomlem  9606  cnfcom2  9609  infxpenc2  9930  adderpqlem  10863  addassnq  10867  distrnq  10870  halfnq  10885  archnq  10889  addclprlem2  10926  addcmpblnr  10978  ltsrpr  10986  m1m1sr  11002  recexsrlem  11012  sqgt0sr  11015  map2psrpr  11019  axi2m1  11068  axcnre  11073  mul02lem2  11308  addrid  11311  cnegex2  11313  addlid  11314  mvrraddi  11395  mvrladdi  11396  mvlladdi  11397  negsubdi  11435  mulneg1  11571  recextlem1  11765  recdiv  11845  divmul13i  11900  mvllmuli  11972  2p2e4  12273  2times  12274  1p2e3  12281  3p2e5  12289  3p3e6  12290  4p2e6  12291  4p3e7  12292  4p4e8  12293  5p2e7  12294  5p3e8  12295  5p4e9  12296  6p2e8  12297  6p3e9  12298  7p2e9  12299  8th4div3  12359  halfpm6th  12361  nneo  12574  9p1e10  12607  dfdec10  12608  num0h  12617  numsuc  12619  dec10p  12648  numma  12649  nummac  12650  numma2c  12651  numadd  12652  numaddc  12653  nummul2c  12655  decaddci  12666  decsubi  12668  5p5e10  12676  6p4e10  12677  7p3e10  12680  8p2e10  12685  decbin0  12745  decbin2  12746  xmulm1  13194  xadddi2  13210  x2times  13212  elfzp1b  13515  elfzm1b  13516  fz0dif1  13520  fz1ssfz0  13537  fz0to4untppr  13544  fz0to5un2tp  13545  fz0sn0fz1  13559  fz0add1fz1  13649  elfz0lmr  13697  fldiv4p1lem1div2  13753  quoremz  13773  quoremnn0ALT  13775  uzrdgxfr  13888  mulexpz  14023  expaddz  14027  sqrecii  14104  sq4e2t8  14120  cu2  14121  i3  14124  iexpcyc  14128  binom2i  14133  binom3  14145  crreczi  14149  discr  14161  3dec  14187  nn0opthlem1  14189  nn0opth2i  14192  faclbnd  14211  bcp1nk  14238  bcpasc  14242  hashp1i  14324  hashxplem  14354  hashpw  14357  hashfun  14358  hashbc  14374  hash7g  14407  ccatlid  14508  pfxccatin12lem2c  14651  revs1  14686  cats1cat  14782  cats2cat  14783  lsws2  14825  lsws3  14826  lsws4  14827  s3s4  14854  s2s5  14855  s5s2  14856  imre  15029  crim  15036  remullem  15049  cnpart  15161  sqrtneglem  15187  absexpz  15226  absimle  15230  sqreulem  15281  amgm2  15291  iseraltlem2  15604  iseraltlem3  15605  modfsummod  15715  binomlem  15750  binom11  15753  arisum  15781  arisum2  15782  pwdif  15789  georeclim  15793  geo2sum  15794  mertenslem1  15805  mertens  15807  prodfrec  15816  fprodm1s  15891  fprodp1s  15892  fprodmodd  15918  fallfacfwd  15957  0risefac  15959  bpolydiflem  15975  bpoly2  15978  bpoly3  15979  bpoly4  15980  fsumcube  15981  efzval  16025  resinval  16058  recosval  16059  efi4p  16060  tan0  16074  efival  16075  sinhval  16077  coshval  16078  cosadd  16088  cos2tsin  16102  ef01bndlem  16107  cos1bnd  16110  cos2bnd  16111  absefib  16121  efieq1re  16122  demoivreALT  16124  eirrlem  16127  rpnnen2lem3  16139  rpnnen2lem11  16147  ruclem7  16159  3dvds  16256  3dvdsdec  16257  3dvds2dec  16258  odd2np1  16266  nn0o1gt2  16306  nn0o  16308  pwp1fsum  16316  divalglem2  16320  divalglem9  16326  5ndvds3  16338  5ndvds6  16339  flodddiv4  16340  m1bits  16365  sadcp1  16380  sadeq  16397  smupp1  16405  smumul  16418  gcdaddmlem  16449  nn0expgcd  16489  3lcm2e6woprm  16540  nn0gcdsq  16677  phiprmpw  16701  prmdiv  16710  prmdiveq  16711  pythagtriplem1  16742  pythagtriplem12  16752  pythagtriplem14  16754  pockthi  16833  infpnlem1  16836  prmreclem4  16845  4sqlem12  16882  4sqlem13  16883  4sqlem19  16889  vdwapun  16900  vdwlem6  16912  0hashbc  16933  prmo2  16966  prmo3  16967  dec5dvds  16990  dec5nprm  16992  dec2nprm  16993  modxai  16994  modxp1i  16996  mod2xnegi  16997  modsubi  16998  gcdmodi  17000  decsplit0b  17005  decsplit1  17007  decsplit  17008  karatsuba  17009  2exp7  17013  2exp8  17014  3exp3  17017  5prm  17034  7prm  17036  11prm  17040  prmlem2  17045  37prm  17046  43prm  17047  83prm  17048  139prm  17049  163prm  17050  317prm  17051  631prm  17052  prmo5  17054  1259lem1  17056  1259lem2  17057  1259lem3  17058  1259lem4  17059  1259lem5  17060  2503lem1  17062  2503lem2  17063  2503lem3  17064  2503prm  17065  4001lem1  17066  4001lem2  17067  4001lem3  17068  4001lem4  17069  4001prm  17070  pwsbas  17405  rcaninv  17716  subsubc  17775  xpccatid  18109  chnub  18543  subsubmgm  18633  subsubm  18739  smndex2dnrinv  18838  mulg2  19011  subsubg  19077  oppgmnd  19281  gsumwrev  19293  psgnunilem2  19422  sylow1lem1  19525  subgslw  19543  sylow3  19560  efginvrel2  19654  efgsfo  19666  frgpnabllem1  19800  gsumzaddlem  19848  gsummptfzsplitl  19860  gsummpt1n0  19892  dprdfid  19946  ablfac1lem  19997  pgpfac1lem3  20006  pgpfaclem1  20010  ablsimpgfindlem1  20036  mgpress  20083  srgbinomlem4  20162  opprrng  20279  unitsubm  20320  subsubrng  20494  subsubrg  20529  cntzsdrg  20733  subdrgint  20734  lsslss  20910  xrsnsgrp  21360  gzrngunit  21386  expghm  21428  pzriprng1ALT  21449  chrid  21478  zrhpsgnmhm  21537  psgndiflemA  21554  frlmip  21731  frlmphl  21734  evlsval  22039  mpff  22065  coe1fzgsumdlem  22245  evl1gsumdlem  22298  matvsca2  22370  mattposvs  22397  m2detleiblem3  22571  m2detleiblem4  22572  cpmidpmat  22815  resstopn  23128  cnmpt1res  23618  ressuss  24204  iscusp2  24243  ucnextcn  24245  txmetcnp  24489  rerest  24746  xrtgioo  24749  xrrest  24750  cnmpopc  24876  xrhmeo  24898  clmvs2  25048  clmnegneg  25058  ncvsm1  25108  ncvspi  25110  cphassir  25169  cphipval2  25195  reust  25335  rrxprds  25343  csbren  25353  rrxdsfi  25365  minveclem2  25380  ovolunlem1a  25451  ovolicc2lem4  25475  uniioombllem5  25542  iblabs  25784  iblabsr  25785  iblmulc2  25786  itgmulc2  25789  limcres  25841  dvfval  25852  dvreslem  25864  dvres2lem  25865  dvcnp2  25875  dvcnp2OLD  25876  cpnres  25893  dvmulbr  25895  dvcobr  25903  dvcobrOLD  25904  dveflem  25937  lhop1lem  25972  lhop2  25974  dvcnvrelem2  25977  plyun0  26156  coeeulem  26183  coeeu  26184  dvply1  26245  dvtaylp  26332  taylthlem2  26336  taylthlem2OLD  26337  taylth  26338  dvradcnv  26384  pserdvlem2  26392  abelthlem8  26403  abelth  26405  sinhalfpilem  26426  cospi  26435  eulerid  26437  cos2pi  26439  ef2kpi  26441  sinhalfpip  26455  sinhalfpim  26456  coshalfpip  26457  coshalfpim  26458  sincosq3sgn  26463  sincosq4sgn  26464  tangtx  26468  sincos4thpi  26476  sincos6thpi  26479  sineq0  26487  tanregt0  26502  logm1  26552  abslogle  26581  tanarg  26582  logcnlem4  26608  advlogexp  26618  cxpsqrt  26666  dvsqrt  26705  dvcnsqrt  26707  cxpcn3  26712  root1cj  26720  cxpeq  26721  logb1  26733  2logb9irr  26759  sqrt2cxp2logb9e3  26763  ang180lem1  26773  ang180lem2  26774  ang180lem3  26775  lawcos  26780  isosctrlem1  26782  isosctrlem2  26783  quad2  26803  1cubrlem  26805  1cubr  26806  dcubic2  26808  mcubic  26811  binom4  26814  dquartlem1  26815  quart1lem  26819  quart1  26820  quartlem1  26821  asinlem  26832  asinlem2  26833  asinlem3a  26834  acosneg  26851  efiasin  26852  asinsinlem  26855  asinsin  26856  acoscos  26857  asin1  26858  acosbnd  26864  atancj  26874  efiatan  26876  atanlogaddlem  26877  efiatan2  26881  2efiatan  26882  tanatan  26883  cosatan  26885  atantan  26887  atanbndlem  26889  atans2  26895  dvatan  26899  atantayl  26901  atantayl2  26902  log2cnv  26908  log2tlbnd  26909  log2ublem2  26911  log2ublem3  26912  log2ub  26913  birthday  26918  jensenlem1  26951  amgmlem  26954  lgamgulmlem2  26994  lgamgulmlem5  26997  lgambdd  27001  ftalem2  27038  ftalem5  27041  ftalem6  27042  basellem2  27046  basellem3  27047  basellem5  27049  basellem8  27052  basellem9  27053  mule1  27112  ppi1i  27132  musum  27155  ppiublem1  27167  ppiub  27169  chtublem  27176  chtub  27177  dchrptlem1  27229  dchrptlem2  27230  bclbnd  27245  bposlem6  27254  bposlem8  27256  bposlem9  27257  lgsdir2lem1  27290  lgsdir2lem2  27291  lgsdir2lem4  27293  lgsdir2lem5  27294  lgsne0  27300  1lgs  27305  gausslemma2dlem0e  27325  gausslemma2dlem0f  27326  gausslemma2dlem3  27333  gausslemma2d  27339  lgseisenlem1  27340  lgseisenlem2  27341  lgseisenlem3  27342  lgseisenlem4  27343  lgseisen  27344  lgsquadlem1  27345  lgsquadlem2  27346  lgsquad2lem1  27349  lgsquad2lem2  27350  m1lgs  27353  2lgslem3a  27361  2lgslem3b  27362  2lgslem3c  27363  2lgslem3d  27364  2lgsoddprmlem3a  27375  2lgsoddprmlem3b  27376  2lgsoddprmlem3c  27377  2lgsoddprmlem3d  27378  addsqnreup  27408  chebbnd1lem2  27435  chebbnd1lem3  27436  rplogsumlem2  27450  dchrisum0flblem1  27473  dchrisum0re  27478  mulog2sumlem2  27500  chpdifbndlem1  27518  pntpbnd1a  27550  pntpbnd2  27552  pntibndlem2  27556  pntibndlem3  27557  pntlemg  27563  pntlemk  27571  pntlemo  27572  no2times  28375  zseo  28380  avgslt1d  28411  avgslt2d  28412  pw2cut2  28419  bdaypw2n0s  28420  remulscllem1  28445  axsegconlem1  28939  ax5seglem7  28957  axlowdimlem3  28966  axlowdimlem16  28979  axlowdimlem17  28980  elntg2  29007  vdegp1bi  29560  vtxdginducedm1  29566  wlkp1lem1  29694  spthispth  29746  cyclnumvtx  29822  2wlkdlem1  29947  2pthd  29962  clwlkclwwlkfo  30033  3wlkdlem1  30183  3pthd  30198  eucrct2eupth  30269  numclwwlk5  30412  numclwwlk7  30415  frgrregord013  30419  ex-fl  30471  ex-mod  30473  ex-exp  30474  ex-bc  30476  ex-lcm  30482  ex-ind-dvds  30485  vc2OLD  30592  vc0  30598  vcm  30600  nvm1  30689  nvpi  30691  nvmtri  30695  nvge0  30697  ipval3  30733  ipidsq  30734  ip0i  30849  ip1ilem  30850  ip2i  30852  ipdirilem  30853  ipasslem10  30863  siilem1  30875  siii  30877  minvecolem2  30899  hvsubid  31050  hvaddsubval  31057  hvmul2negi  31072  hvadd12i  31081  hv2times  31085  hvnegdii  31086  hvaddcani  31089  hi01  31120  hisubcomi  31128  normlem0  31133  normlem1  31134  normlem3  31136  normlem9  31142  bcseqi  31144  normsqi  31156  norm-ii-i  31161  normsubi  31165  norm3difi  31171  norm3adifii  31172  normpar2i  31180  polid2i  31181  polidi  31182  chdmm2i  31502  chj12i  31546  spanunsni  31603  qlaxr5i  31659  osumcor2i  31668  spansnji  31670  pjadjii  31698  pjinormii  31700  pjsslem  31703  pjpythi  31746  mayete3i  31752  mayetes3i  31753  hoadd12i  31801  honegneg  31830  ho2times  31843  hoaddsubi  31845  hosd1i  31846  hosd2i  31847  honpncani  31851  lnopeq0lem1  32029  lnopunilem1  32034  lnophmlem2  32041  lnfn0i  32066  nmopcoadji  32125  nmopcoadj2i  32126  opsqrlem1  32164  opsqrlem5  32168  opsqrlem6  32169  pjclem3  32221  stadd3i  32272  mddmd2  32333  mdexchi  32359  cvexchlem  32392  atomli  32406  atordi  32408  atabs2i  32426  mdsymlem1  32427  iuninc  32584  suppss2f  32665  mptiffisupp  32721  suppss3  32751  binom2subadd  32770  pythagreim  32774  dfdec100  32860  dpfrac1  32922  decdiv10  32926  dpmul100  32927  dp3mul10  32928  dpmul1000  32929  dpexpp1  32938  dpadd2  32940  dpadd  32941  dpmul  32943  dpmul4  32944  threehalves  32945  1mhdrd  32946  pfxlsw2ccat  32981  ccatws1f1olast  32983  gsummulsubdishift1s  33102  gsummulsubdishift2s  33103  cyc2fv1  33152  cyc2fv2  33153  cycpmco2lem4  33160  cycpmco2lem5  33161  cyc3fv1  33168  cyc3fv2  33169  cyc3fv3  33170  archirngz  33220  gsumvsca2  33258  elrgspnlem4  33276  subsdrg  33329  nn0omnd  33374  nn0archi  33377  xrge0slmod  33378  opprabs  33512  ressply1evls1  33595  extvfvcl  33650  mplmulmvr  33653  esplyfvn  33682  vietalem  33684  vieta  33685  resssra  33692  lsssra  33693  fedgmullem1  33735  fedgmullem2  33736  fedgmul  33737  fldsdrgfldext2  33768  fldgenfldext  33774  fldextrspunlem1  33781  fldextrspunfld  33782  fldextrspundgdvdslem  33786  fldextrspundgdvds  33787  algextdeglem1  33823  algextdeglem4  33826  constrrtcclem  33840  constrmulcl  33877  constrinvcl  33879  2sqr3minply  33886  cos9thpiminplylem4  33891  cos9thpiminplylem5  33892  lmatfvlem  33921  sqsscirc1  34014  cnvordtrestixx  34019  raddcn  34035  xrge0iifhom  34043  xrge0mulc1cn  34047  xrge0tmd  34051  lmlimxrge0  34054  qqhucn  34098  rrhcn  34103  qqtopn  34117  rrhqima  34120  brfae  34354  inelcarsg  34417  cndprobnul  34543  isrrvv  34549  ballotlem1  34593  ballotlem2  34595  ballotlemi1  34609  ballotlemii  34610  ballotlemic  34613  ballotlem1c  34614  ballotlemfrceq  34635  ballotth  34644  ofcs2  34651  signsvtn0  34676  signstfveq0  34683  signsvtp  34689  signsvtn  34690  signsvfpn  34691  signsvfnn  34692  signshf  34694  hashreprin  34726  reprfz1  34730  chtvalz  34735  breprexp  34739  breprexpnat  34740  hgt750lemd  34754  hgt750lem  34757  hgt750lem2  34758  subfacp1lem1  35322  subfacp1lem5  35327  subfacp1lem6  35328  subfaclim  35331  cvmliftlem5  35432  cvmliftlem8  35435  cvmliftlem10  35437  cvmliftlem13  35439  cvmlift2lem6  35451  cvmlift2lem12  35457  problem1  35808  problem2  35809  problem4  35811  quad3  35813  iexpire  35878  itgeq12i  36349  sin2h  37750  poimirlem16  37776  poimirlem17  37777  poimirlem18  37778  poimirlem19  37779  poimirlem20  37780  poimirlem21  37781  poimirlem22  37782  poimirlem26  37786  mblfinlem3  37799  ismblfin  37801  itg2addnclem3  37813  iblabsnc  37824  iblmulc2nc  37825  itgmulc2nc  37828  ftc1cnnc  37832  ftc1anclem6  37838  ftc1anclem7  37839  ftc1anclem8  37840  dvasin  37844  fdc  37885  heiborlem4  37954  heiborlem6  37956  dalem24  39896  pmod2iN  40048  cdleme9  40452  cdleme20aN  40508  cdleme22e  40543  cdleme22eALTN  40544  cdleme25cv  40557  cdleme29b  40574  cdlemh1  41014  cdlemh2  41015  cdlemk35  41111  cdlemkid1  41121  12gcd5e1  42196  60gcd7e1  42198  420gcd8e4  42199  12lcm5e60  42201  420lcm8e840  42204  lcm1un  42206  lcm2un  42207  lcm3un  42208  lcm4un  42209  lcm5un  42210  lcm6un  42211  lcm7un  42212  lcm8un  42213  3factsumint1  42214  3factsumint3  42216  lcmineqlem10  42231  3exp7  42246  3lexlogpow5ineq1  42247  3lexlogpow5ineq5  42253  aks4d1p1  42269  5bc2eq10  42335  2ap1caineq  42338  aks5lem3a  42382  aks5lem7  42393  1p3e4  42456  sqmid3api  42480  sqn5i  42482  sqdeccom12  42486  235t711  42502  cxpi11d  42540  sin2t3rdpi  42550  cos2t3rdpi  42551  re1m1e0m0  42594  readdlid  42600  remul02  42602  sn-1ticom  42632  sn-mullid  42633  sn-0tie0  42648  sn-mul02  42649  sn-inelr  42684  mhphf2  42783  flt4lem5e  42841  sum9cubes  42857  pellexlem5  43017  reglog1  43080  jm2.23  43180  jm2.27c  43191  lnmlsslnm  43265  lmhmlnmsplit  43271  areaquad  43400  oaomoencom  43501  resqrtvalex  43828  imsqrtvalex  43829  cotrclrcl  43925  inductionexd  44338  hashnzfz2  44504  lhe4.4ex1a  44512  binomcxplemdvsum  44538  binomcxplemnotnn0  44539  binomcxp  44540  sineq0ALT  45119  unirnmapsn  45400  fzisoeu  45490  fsummulc1f  45759  fprodexp  45782  constlimc  45812  sumnnodd  45818  limcresiooub  45828  limcresioolb  45829  cncfshiftioo  46078  fperdvper  46105  dvnmul  46129  dvmptfprod  46131  itgsinexplem1  46140  stoweidlem11  46197  stoweidlem13  46199  stoweidlem26  46212  stoweidlem34  46220  wallispilem4  46254  wallispi2lem1  46257  wallispi2lem2  46258  stirlinglem11  46270  dirkerper  46282  dirkertrigeqlem1  46284  dirkertrigeqlem3  46286  dirkercncflem1  46289  dirkercncflem4  46292  fourierdlem30  46323  fourierdlem32  46325  fourierdlem33  46326  fourierdlem42  46335  fourierdlem46  46338  fourierdlem47  46339  fourierdlem57  46349  fourierdlem60  46352  fourierdlem61  46353  fourierdlem62  46354  fourierdlem68  46360  fourierdlem73  46365  fourierdlem79  46371  fourierdlem89  46381  fourierdlem90  46382  fourierdlem91  46383  fourierdlem96  46388  fourierdlem97  46389  fourierdlem98  46390  fourierdlem99  46391  fourierdlem100  46392  fourierdlem103  46395  fourierdlem104  46396  fourierdlem108  46400  fourierdlem110  46402  fourierdlem113  46405  sqwvfoura  46414  sqwvfourb  46415  fourierswlem  46416  fouriersw  46417  fouriercn  46418  etransclem4  46424  etransclem7  46427  etransclem23  46443  etransclem24  46444  etransclem25  46445  etransclem26  46446  etransclem31  46451  etransclem32  46452  etransclem35  46455  etransclem37  46457  etransclem46  46466  rrndistlt  46476  sge0tsms  46566  sge0xaddlem2  46620  vonioolem2  46867  ormklocald  47060  natlocalincr  47062  nthrucw  47072  1t10e1p1e11  47498  deccarry  47499  1fzopredsuc  47512  ceil5half3  47528  minusmodnep2tmod  47541  m1mod0mod1  47542  8mod5e3  47548  modmkpkne  47549  modm1p1ne  47558  iccpartgt  47615  fmtno0  47728  fmtno1  47729  fmtnorec2  47731  fmtno2  47738  fmtno3  47739  fmtno4  47740  fmtno5  47745  257prm  47749  fmtnofac1  47758  fmtno4prmfac  47760  fmtno4prmfac193  47761  fmtno4nprmfac193  47762  m2prm  47779  m3prm  47780  flsqrt5  47782  3ndvds4  47783  139prmALT  47784  31prm  47785  127prm  47787  m11nprm  47789  lighneallem2  47794  lighneallem3  47795  3exp4mod41  47804  41prothprmlem1  47805  41prothprmlem2  47806  41prothprm  47807  m1expevenALTV  47835  1oddALTV  47878  6even  47899  8even  47901  2exp340mod341  47921  341fppr2  47922  4fppr1  47923  8exp8mod9  47924  9fppr8  47925  nfermltl8rev  47930  gbpart7  47955  gbpart9  47957  gbpart11  47958  sbgoldbo  47975  bgoldbtbndlem1  47993  tgoldbachlt  48004  gpg3kgrtriexlem2  48272  gpg3kgrtriexlem4  48274  gpg3kgrtriexlem6  48276  gpg3kgrtriex  48277  gpgprismgr4cycllem3  48285  gpgprismgr4cycllem11  48293  pgnbgreunbgrlem2lem1  48302  pgnbgreunbgrlem2lem2  48303  pgnbgreunbgrlem4  48307  pgnbgreunbgrlem5lem1  48308  pgnbgreunbgrlem5lem2  48309  gpg5edgnedg  48318  altgsumbcALT  48541  lincfsuppcl  48601  linccl  48602  lincvalsn  48605  lincdifsn  48612  lincsum  48617  lincscm  48618  lindslinindimp2lem4  48649  lindslinindsimp2lem5  48650  snlindsntor  48659  lincresunit3lem2  48668  zlmodzxzldeplem3  48690  ldepsnlinc  48696  nn0sumshdiglemA  48807  nn0sumshdiglemB  48808  ackval2  48870  ackval2012  48879  ackval3012  48880  ackval41a  48882  ackval42  48884  ackval42a  48885  affinecomb1  48890  rrx2linest  48930  itschlc0yqe  48948  itsclc0yqsollem1  48950  itscnhlc0xyqsol  48953  itschlc0xyqsol1  48954  itsclquadb  48964  2itscplem2  48967  itscnhlinecirc02plem2  48971  oppcup  49394  natoppf  49416  islmd  49852  iscmd  49853  lmddu  49854  sinh-conventional  49926  onetansqsecsq  49948  cotsqcscsq  49949  mvlraddi  49958  mvlrmuli  49964  amgmwlem  49989  amgmlemALT  49990