Theorem oveq1i 7397

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

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

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390

This theorem is referenced by:  caov12  7617  caov411  7621  omopthlem1  8623  map1  9011  pw2eng  9047  fsuppunbi  9340  cnfcomlem  9652  cnfcom2  9655  infxpenc2  9975  adderpqlem  10907  addassnq  10911  distrnq  10914  halfnq  10929  archnq  10933  addclprlem2  10970  addcmpblnr  11022  ltsrpr  11030  m1m1sr  11046  recexsrlem  11056  sqgt0sr  11059  map2psrpr  11063  axi2m1  11112  axcnre  11117  mul02lem2  11351  addrid  11354  cnegex2  11356  addlid  11357  mvrraddi  11438  mvrladdi  11439  mvlladdi  11440  negsubdi  11478  mulneg1  11614  recextlem1  11808  recdiv  11888  divmul13i  11943  mvllmuli  12015  2p2e4  12316  2times  12317  1p2e3  12324  3p2e5  12332  3p3e6  12333  4p2e6  12334  4p3e7  12335  4p4e8  12336  5p2e7  12337  5p3e8  12338  5p4e9  12339  6p2e8  12340  6p3e9  12341  7p2e9  12342  8th4div3  12402  halfpm6th  12404  nneo  12618  9p1e10  12651  dfdec10  12652  num0h  12661  numsuc  12663  dec10p  12692  numma  12693  nummac  12694  numma2c  12695  numadd  12696  numaddc  12697  nummul2c  12699  decaddci  12710  decsubi  12712  5p5e10  12720  6p4e10  12721  7p3e10  12724  8p2e10  12729  decbin0  12789  decbin2  12790  xmulm1  13241  xadddi2  13257  x2times  13259  elfzp1b  13562  elfzm1b  13563  fz0dif1  13567  fz1ssfz0  13584  fz0to4untppr  13591  fz0to5un2tp  13592  fz0sn0fz1  13606  fz0add1fz1  13696  elfz0lmr  13743  fldiv4p1lem1div2  13797  quoremz  13817  quoremnn0ALT  13819  uzrdgxfr  13932  mulexpz  14067  expaddz  14071  sqrecii  14148  sq4e2t8  14164  cu2  14165  i3  14168  iexpcyc  14172  binom2i  14177  binom3  14189  crreczi  14193  discr  14205  3dec  14231  nn0opthlem1  14233  nn0opth2i  14236  faclbnd  14255  bcp1nk  14282  bcpasc  14286  hashp1i  14368  hashxplem  14398  hashpw  14401  hashfun  14402  hashbc  14418  hash7g  14451  ccatlid  14551  pfxccatin12lem2c  14695  revs1  14730  cats1cat  14827  cats2cat  14828  lsws2  14870  lsws3  14871  lsws4  14872  s3s4  14899  s2s5  14900  s5s2  14901  imre  15074  crim  15081  remullem  15094  cnpart  15206  sqrtneglem  15232  absexpz  15271  absimle  15275  sqreulem  15326  amgm2  15336  iseraltlem2  15649  iseraltlem3  15650  modfsummod  15760  binomlem  15795  binom11  15798  arisum  15826  arisum2  15827  pwdif  15834  georeclim  15838  geo2sum  15839  mertenslem1  15850  mertens  15852  prodfrec  15861  fprodm1s  15936  fprodp1s  15937  fprodmodd  15963  fallfacfwd  16002  0risefac  16004  bpolydiflem  16020  bpoly2  16023  bpoly3  16024  bpoly4  16025  fsumcube  16026  efzval  16070  resinval  16103  recosval  16104  efi4p  16105  tan0  16119  efival  16120  sinhval  16122  coshval  16123  cosadd  16133  cos2tsin  16147  ef01bndlem  16152  cos1bnd  16155  cos2bnd  16156  absefib  16166  efieq1re  16167  demoivreALT  16169  eirrlem  16172  rpnnen2lem3  16184  rpnnen2lem11  16192  ruclem7  16204  3dvds  16301  3dvdsdec  16302  3dvds2dec  16303  odd2np1  16311  nn0o1gt2  16351  nn0o  16353  pwp1fsum  16361  divalglem2  16365  divalglem9  16371  5ndvds3  16383  5ndvds6  16384  flodddiv4  16385  m1bits  16410  sadcp1  16425  sadeq  16442  smupp1  16450  smumul  16463  gcdaddmlem  16494  nn0expgcd  16534  3lcm2e6woprm  16585  nn0gcdsq  16722  phiprmpw  16746  prmdiv  16755  prmdiveq  16756  pythagtriplem1  16787  pythagtriplem12  16797  pythagtriplem14  16799  pockthi  16878  infpnlem1  16881  prmreclem4  16890  4sqlem12  16927  4sqlem13  16928  4sqlem19  16934  vdwapun  16945  vdwlem6  16957  0hashbc  16978  prmo2  17011  prmo3  17012  dec5dvds  17035  dec5nprm  17037  dec2nprm  17038  modxai  17039  modxp1i  17041  mod2xnegi  17042  modsubi  17043  gcdmodi  17045  decsplit0b  17050  decsplit1  17052  decsplit  17053  karatsuba  17054  2exp7  17058  2exp8  17059  3exp3  17062  5prm  17079  7prm  17081  11prm  17085  prmlem2  17090  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  prmo5  17099  1259lem1  17101  1259lem2  17102  1259lem3  17103  1259lem4  17104  1259lem5  17105  2503lem1  17107  2503lem2  17108  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  pwsbas  17450  rcaninv  17756  subsubc  17815  xpccatid  18149  subsubmgm  18637  subsubm  18743  smndex2dnrinv  18842  mulg2  19015  subsubg  19081  oppgmnd  19286  gsumwrev  19298  psgnunilem2  19425  sylow1lem1  19528  subgslw  19546  sylow3  19563  efginvrel2  19657  efgsfo  19669  frgpnabllem1  19803  gsumzaddlem  19851  gsummptfzsplitl  19863  gsummpt1n0  19895  dprdfid  19949  ablfac1lem  20000  pgpfac1lem3  20009  pgpfaclem1  20013  ablsimpgfindlem1  20039  mgpress  20059  srgbinomlem4  20138  opprrng  20254  unitsubm  20295  subsubrng  20472  subsubrg  20507  cntzsdrg  20711  subdrgint  20712  lsslss  20867  xrsnsgrp  21319  gzrngunit  21350  expghm  21385  pzriprng1ALT  21406  chrid  21435  zrhpsgnmhm  21493  psgndiflemA  21510  frlmip  21687  frlmphl  21690  evlsval  21993  mpff  22011  coe1fzgsumdlem  22190  evl1gsumdlem  22243  matvsca2  22315  mattposvs  22342  m2detleiblem3  22516  m2detleiblem4  22517  cpmidpmat  22760  resstopn  23073  cnmpt1res  23563  ressuss  24150  iscusp2  24189  ucnextcn  24191  txmetcnp  24435  rerest  24692  xrtgioo  24695  xrrest  24696  cnmpopc  24822  xrhmeo  24844  clmvs2  24994  clmnegneg  25004  ncvsm1  25054  ncvspi  25056  cphassir  25115  cphipval2  25141  reust  25281  rrxprds  25289  csbren  25299  rrxdsfi  25311  minveclem2  25326  ovolunlem1a  25397  ovolicc2lem4  25421  uniioombllem5  25488  iblabs  25730  iblabsr  25731  iblmulc2  25732  itgmulc2  25735  limcres  25787  dvfval  25798  dvreslem  25810  dvres2lem  25811  dvcnp2  25821  dvcnp2OLD  25822  cpnres  25839  dvmulbr  25841  dvcobr  25849  dvcobrOLD  25850  dveflem  25883  lhop1lem  25918  lhop2  25920  dvcnvrelem2  25923  plyun0  26102  coeeulem  26129  coeeu  26130  dvply1  26191  dvtaylp  26278  taylthlem2  26282  taylthlem2OLD  26283  taylth  26284  dvradcnv  26330  pserdvlem2  26338  abelthlem8  26349  abelth  26351  sinhalfpilem  26372  cospi  26381  eulerid  26383  cos2pi  26385  ef2kpi  26387  sinhalfpip  26401  sinhalfpim  26402  coshalfpip  26403  coshalfpim  26404  sincosq3sgn  26409  sincosq4sgn  26410  tangtx  26414  sincos4thpi  26422  sincos6thpi  26425  sineq0  26433  tanregt0  26448  logm1  26498  abslogle  26527  tanarg  26528  logcnlem4  26554  advlogexp  26564  cxpsqrt  26612  dvsqrt  26651  dvcnsqrt  26653  cxpcn3  26658  root1cj  26666  cxpeq  26667  logb1  26679  2logb9irr  26705  sqrt2cxp2logb9e3  26709  ang180lem1  26719  ang180lem2  26720  ang180lem3  26721  lawcos  26726  isosctrlem1  26728  isosctrlem2  26729  quad2  26749  1cubrlem  26751  1cubr  26752  dcubic2  26754  mcubic  26757  binom4  26760  dquartlem1  26761  quart1lem  26765  quart1  26766  quartlem1  26767  asinlem  26778  asinlem2  26779  asinlem3a  26780  acosneg  26797  efiasin  26798  asinsinlem  26801  asinsin  26802  acoscos  26803  asin1  26804  acosbnd  26810  atancj  26820  efiatan  26822  atanlogaddlem  26823  efiatan2  26827  2efiatan  26828  tanatan  26829  cosatan  26831  atantan  26833  atanbndlem  26835  atans2  26841  dvatan  26845  atantayl  26847  atantayl2  26848  log2cnv  26854  log2tlbnd  26855  log2ublem2  26857  log2ublem3  26858  log2ub  26859  birthday  26864  jensenlem1  26897  amgmlem  26900  lgamgulmlem2  26940  lgamgulmlem5  26943  lgambdd  26947  ftalem2  26984  ftalem5  26987  ftalem6  26988  basellem2  26992  basellem3  26993  basellem5  26995  basellem8  26998  basellem9  26999  mule1  27058  ppi1i  27078  musum  27101  ppiublem1  27113  ppiub  27115  chtublem  27122  chtub  27123  dchrptlem1  27175  dchrptlem2  27176  bclbnd  27191  bposlem6  27200  bposlem8  27202  bposlem9  27203  lgsdir2lem1  27236  lgsdir2lem2  27237  lgsdir2lem4  27239  lgsdir2lem5  27240  lgsne0  27246  1lgs  27251  gausslemma2dlem0e  27271  gausslemma2dlem0f  27272  gausslemma2dlem3  27279  gausslemma2d  27285  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgseisen  27290  lgsquadlem1  27291  lgsquadlem2  27292  lgsquad2lem1  27295  lgsquad2lem2  27296  m1lgs  27299  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2lgsoddprmlem3a  27321  2lgsoddprmlem3b  27322  2lgsoddprmlem3c  27323  2lgsoddprmlem3d  27324  addsqnreup  27354  chebbnd1lem2  27381  chebbnd1lem3  27382  rplogsumlem2  27396  dchrisum0flblem1  27419  dchrisum0re  27424  mulog2sumlem2  27446  chpdifbndlem1  27464  pntpbnd1a  27496  pntpbnd2  27498  pntibndlem2  27502  pntibndlem3  27503  pntlemg  27509  pntlemk  27517  pntlemo  27518  no2times  28303  zseo  28308  remulscllem1  28351  axsegconlem1  28844  ax5seglem7  28862  axlowdimlem3  28871  axlowdimlem16  28884  axlowdimlem17  28885  elntg2  28912  vdegp1bi  29465  vtxdginducedm1  29471  wlkp1lem1  29601  spthispth  29654  cyclnumvtx  29730  2wlkdlem1  29855  2pthd  29870  clwlkclwwlkfo  29938  3wlkdlem1  30088  3pthd  30103  eucrct2eupth  30174  numclwwlk5  30317  numclwwlk7  30320  frgrregord013  30324  ex-fl  30376  ex-mod  30378  ex-exp  30379  ex-bc  30381  ex-lcm  30387  ex-ind-dvds  30390  vc2OLD  30497  vc0  30503  vcm  30505  nvm1  30594  nvpi  30596  nvmtri  30600  nvge0  30602  ipval3  30638  ipidsq  30639  ip0i  30754  ip1ilem  30755  ip2i  30757  ipdirilem  30758  ipasslem10  30768  siilem1  30780  siii  30782  minvecolem2  30804  hvsubid  30955  hvaddsubval  30962  hvmul2negi  30977  hvadd12i  30986  hv2times  30990  hvnegdii  30991  hvaddcani  30994  hi01  31025  hisubcomi  31033  normlem0  31038  normlem1  31039  normlem3  31041  normlem9  31047  bcseqi  31049  normsqi  31061  norm-ii-i  31066  normsubi  31070  norm3difi  31076  norm3adifii  31077  normpar2i  31085  polid2i  31086  polidi  31087  chdmm2i  31407  chj12i  31451  spanunsni  31508  qlaxr5i  31564  osumcor2i  31573  spansnji  31575  pjadjii  31603  pjinormii  31605  pjsslem  31608  pjpythi  31651  mayete3i  31657  mayetes3i  31658  hoadd12i  31706  honegneg  31735  ho2times  31748  hoaddsubi  31750  hosd1i  31751  hosd2i  31752  honpncani  31756  lnopeq0lem1  31934  lnopunilem1  31939  lnophmlem2  31946  lnfn0i  31971  nmopcoadji  32030  nmopcoadj2i  32031  opsqrlem1  32069  opsqrlem5  32073  opsqrlem6  32074  pjclem3  32126  stadd3i  32177  mddmd2  32238  mdexchi  32264  cvexchlem  32297  atomli  32311  atordi  32313  atabs2i  32331  mdsymlem1  32332  iuninc  32489  suppss2f  32562  mptiffisupp  32616  suppss3  32647  binom2subadd  32665  pythagreim  32669  dfdec100  32755  dpfrac1  32812  decdiv10  32816  dpmul100  32817  dp3mul10  32818  dpmul1000  32819  dpexpp1  32828  dpadd2  32830  dpadd  32831  dpmul  32833  dpmul4  32834  threehalves  32835  1mhdrd  32836  pfxlsw2ccat  32872  ccatws1f1olast  32874  chnub  32938  cyc2fv1  33078  cyc2fv2  33079  cycpmco2lem4  33086  cycpmco2lem5  33087  cyc3fv1  33094  cyc3fv2  33095  cyc3fv3  33096  archirngz  33143  gsumvsca2  33180  elrgspnlem4  33196  subsdrg  33248  nn0omnd  33316  nn0archi  33318  xrge0slmod  33319  opprabs  33453  ressply1evls1  33534  resssra  33583  lsssra  33584  fedgmullem1  33625  fedgmullem2  33626  fedgmul  33627  fldsdrgfldext2  33658  fldgenfldext  33663  fldextrspunlem1  33670  fldextrspunfld  33671  fldextrspundgdvdslem  33675  fldextrspundgdvds  33676  algextdeglem1  33707  algextdeglem4  33710  constrrtcclem  33724  constrmulcl  33761  constrinvcl  33763  2sqr3minply  33770  cos9thpiminplylem4  33775  cos9thpiminplylem5  33776  lmatfvlem  33805  sqsscirc1  33898  cnvordtrestixx  33903  raddcn  33919  xrge0iifhom  33927  xrge0mulc1cn  33931  xrge0tmd  33935  lmlimxrge0  33938  qqhucn  33982  rrhcn  33987  qqtopn  34001  rrhqima  34004  brfae  34238  inelcarsg  34302  cndprobnul  34428  isrrvv  34434  ballotlem1  34478  ballotlem2  34480  ballotlemi1  34494  ballotlemii  34495  ballotlemic  34498  ballotlem1c  34499  ballotlemfrceq  34520  ballotth  34529  ofcs2  34536  signsvtn0  34561  signstfveq0  34568  signsvtp  34574  signsvtn  34575  signsvfpn  34576  signsvfnn  34577  signshf  34579  hashreprin  34611  reprfz1  34615  chtvalz  34620  breprexp  34624  breprexpnat  34625  hgt750lemd  34639  hgt750lem  34642  hgt750lem2  34643  subfacp1lem1  35166  subfacp1lem5  35171  subfacp1lem6  35172  subfaclim  35175  cvmliftlem5  35276  cvmliftlem8  35279  cvmliftlem10  35281  cvmliftlem13  35283  cvmlift2lem6  35295  cvmlift2lem12  35301  problem1  35652  problem2  35653  problem4  35655  quad3  35657  iexpire  35722  itgeq12i  36194  sin2h  37604  poimirlem16  37630  poimirlem17  37631  poimirlem18  37632  poimirlem19  37633  poimirlem20  37634  poimirlem21  37635  poimirlem22  37636  poimirlem26  37640  mblfinlem3  37653  ismblfin  37655  itg2addnclem3  37667  iblabsnc  37678  iblmulc2nc  37679  itgmulc2nc  37682  ftc1cnnc  37686  ftc1anclem6  37692  ftc1anclem7  37693  ftc1anclem8  37694  dvasin  37698  fdc  37739  heiborlem4  37808  heiborlem6  37810  dalem24  39691  pmod2iN  39843  cdleme9  40247  cdleme20aN  40303  cdleme22e  40338  cdleme22eALTN  40339  cdleme25cv  40352  cdleme29b  40369  cdlemh1  40809  cdlemh2  40810  cdlemk35  40906  cdlemkid1  40916  12gcd5e1  41991  60gcd7e1  41993  420gcd8e4  41994  12lcm5e60  41996  420lcm8e840  41999  lcm1un  42001  lcm2un  42002  lcm3un  42003  lcm4un  42004  lcm5un  42005  lcm6un  42006  lcm7un  42007  lcm8un  42008  3factsumint1  42009  3factsumint3  42011  lcmineqlem10  42026  3exp7  42041  3lexlogpow5ineq1  42042  3lexlogpow5ineq5  42048  aks4d1p1  42064  5bc2eq10  42130  2ap1caineq  42133  aks5lem3a  42177  aks5lem7  42188  1p3e4  42247  sqmid3api  42271  sqn5i  42273  sqdeccom12  42277  235t711  42293  cxpi11d  42331  sin2t3rdpi  42341  cos2t3rdpi  42342  re1m1e0m0  42385  readdlid  42391  remul02  42393  sn-1ticom  42423  sn-mullid  42424  sn-0tie0  42439  sn-mul02  42440  sn-inelr  42475  mhphf2  42586  flt4lem5e  42644  sum9cubes  42660  pellexlem5  42821  reglog1  42884  jm2.23  42985  jm2.27c  42996  lnmlsslnm  43070  lmhmlnmsplit  43076  areaquad  43205  oaomoencom  43306  resqrtvalex  43634  imsqrtvalex  43635  cotrclrcl  43731  inductionexd  44144  hashnzfz2  44310  lhe4.4ex1a  44318  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  binomcxp  44346  sineq0ALT  44926  unirnmapsn  45208  fzisoeu  45298  fsummulc1f  45569  fprodexp  45592  constlimc  45622  sumnnodd  45628  limcresiooub  45640  limcresioolb  45641  cncfshiftioo  45890  fperdvper  45917  dvnmul  45941  dvmptfprod  45943  itgsinexplem1  45952  stoweidlem11  46009  stoweidlem13  46011  stoweidlem26  46024  stoweidlem34  46032  wallispilem4  46066  wallispi2lem1  46069  wallispi2lem2  46070  stirlinglem11  46082  dirkerper  46094  dirkertrigeqlem1  46096  dirkertrigeqlem3  46098  dirkercncflem1  46101  dirkercncflem4  46104  fourierdlem30  46135  fourierdlem32  46137  fourierdlem33  46138  fourierdlem42  46147  fourierdlem46  46150  fourierdlem47  46151  fourierdlem57  46161  fourierdlem60  46164  fourierdlem61  46165  fourierdlem62  46166  fourierdlem68  46172  fourierdlem73  46177  fourierdlem79  46183  fourierdlem89  46193  fourierdlem90  46194  fourierdlem91  46195  fourierdlem96  46200  fourierdlem97  46201  fourierdlem98  46202  fourierdlem99  46203  fourierdlem100  46204  fourierdlem103  46207  fourierdlem104  46208  fourierdlem108  46212  fourierdlem110  46214  fourierdlem113  46217  sqwvfoura  46226  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  fouriercn  46230  etransclem4  46236  etransclem7  46239  etransclem23  46255  etransclem24  46256  etransclem25  46257  etransclem26  46258  etransclem31  46263  etransclem32  46264  etransclem35  46267  etransclem37  46269  etransclem46  46278  rrndistlt  46288  sge0tsms  46378  sge0xaddlem2  46432  vonioolem2  46679  ormklocald  46872  natlocalincr  46874  upwordsing  46882  tworepnotupword  46884  1t10e1p1e11  47311  deccarry  47312  1fzopredsuc  47325  ceil5half3  47341  minusmodnep2tmod  47354  m1mod0mod1  47355  8mod5e3  47361  modmkpkne  47362  modm1p1ne  47371  iccpartgt  47428  fmtno0  47541  fmtno1  47542  fmtnorec2  47544  fmtno2  47551  fmtno3  47552  fmtno4  47553  fmtno5  47558  257prm  47562  fmtnofac1  47571  fmtno4prmfac  47573  fmtno4prmfac193  47574  fmtno4nprmfac193  47575  m2prm  47592  m3prm  47593  flsqrt5  47595  3ndvds4  47596  139prmALT  47597  31prm  47598  127prm  47600  m11nprm  47602  lighneallem2  47607  lighneallem3  47608  3exp4mod41  47617  41prothprmlem1  47618  41prothprmlem2  47619  41prothprm  47620  m1expevenALTV  47648  1oddALTV  47691  6even  47712  8even  47714  2exp340mod341  47734  341fppr2  47735  4fppr1  47736  8exp8mod9  47737  9fppr8  47738  nfermltl8rev  47743  gbpart7  47768  gbpart9  47770  gbpart11  47771  sbgoldbo  47788  bgoldbtbndlem1  47806  tgoldbachlt  47817  gpg3kgrtriexlem2  48075  gpg3kgrtriexlem4  48077  gpg3kgrtriexlem6  48079  gpg3kgrtriex  48080  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem11  48095  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  altgsumbcALT  48341  lincfsuppcl  48402  linccl  48403  lincvalsn  48406  lincdifsn  48413  lincsum  48418  lincscm  48419  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  snlindsntor  48460  lincresunit3lem2  48469  zlmodzxzldeplem3  48491  ldepsnlinc  48497  nn0sumshdiglemA  48608  nn0sumshdiglemB  48609  ackval2  48671  ackval2012  48680  ackval3012  48681  ackval41a  48683  ackval42  48685  ackval42a  48686  affinecomb1  48691  rrx2linest  48731  itschlc0yqe  48749  itsclc0yqsollem1  48751  itscnhlc0xyqsol  48754  itschlc0xyqsol1  48755  itsclquadb  48765  2itscplem2  48768  itscnhlinecirc02plem2  48772  oppcup  49196  natoppf  49218  islmd  49654  iscmd  49655  lmddu  49656  sinh-conventional  49728  onetansqsecsq  49750  cotsqcscsq  49751  mvlraddi  49760  mvlrmuli  49766  amgmwlem  49791  amgmlemALT  49792