Theorem oveq1i 7356

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-iota 6437  df-fv 6489  df-ov 7349

This theorem is referenced by:  caov12  7574  caov411  7578  omopthlem1  8574  map1  8962  pw2eng  8996  fsuppunbi  9273  cnfcomlem  9589  cnfcom2  9592  infxpenc2  9913  adderpqlem  10845  addassnq  10849  distrnq  10852  halfnq  10867  archnq  10871  addclprlem2  10908  addcmpblnr  10960  ltsrpr  10968  m1m1sr  10984  recexsrlem  10994  sqgt0sr  10997  map2psrpr  11001  axi2m1  11050  axcnre  11055  mul02lem2  11290  addrid  11293  cnegex2  11295  addlid  11296  mvrraddi  11377  mvrladdi  11378  mvlladdi  11379  negsubdi  11417  mulneg1  11553  recextlem1  11747  recdiv  11827  divmul13i  11882  mvllmuli  11954  2p2e4  12255  2times  12256  1p2e3  12263  3p2e5  12271  3p3e6  12272  4p2e6  12273  4p3e7  12274  4p4e8  12275  5p2e7  12276  5p3e8  12277  5p4e9  12278  6p2e8  12279  6p3e9  12280  7p2e9  12281  8th4div3  12341  halfpm6th  12343  nneo  12557  9p1e10  12590  dfdec10  12591  num0h  12600  numsuc  12602  dec10p  12631  numma  12632  nummac  12633  numma2c  12634  numadd  12635  numaddc  12636  nummul2c  12638  decaddci  12649  decsubi  12651  5p5e10  12659  6p4e10  12660  7p3e10  12663  8p2e10  12668  decbin0  12728  decbin2  12729  xmulm1  13180  xadddi2  13196  x2times  13198  elfzp1b  13501  elfzm1b  13502  fz0dif1  13506  fz1ssfz0  13523  fz0to4untppr  13530  fz0to5un2tp  13531  fz0sn0fz1  13545  fz0add1fz1  13635  elfz0lmr  13683  fldiv4p1lem1div2  13739  quoremz  13759  quoremnn0ALT  13761  uzrdgxfr  13874  mulexpz  14009  expaddz  14013  sqrecii  14090  sq4e2t8  14106  cu2  14107  i3  14110  iexpcyc  14114  binom2i  14119  binom3  14131  crreczi  14135  discr  14147  3dec  14173  nn0opthlem1  14175  nn0opth2i  14178  faclbnd  14197  bcp1nk  14224  bcpasc  14228  hashp1i  14310  hashxplem  14340  hashpw  14343  hashfun  14344  hashbc  14360  hash7g  14393  ccatlid  14494  pfxccatin12lem2c  14637  revs1  14672  cats1cat  14768  cats2cat  14769  lsws2  14811  lsws3  14812  lsws4  14813  s3s4  14840  s2s5  14841  s5s2  14842  imre  15015  crim  15022  remullem  15035  cnpart  15147  sqrtneglem  15173  absexpz  15212  absimle  15216  sqreulem  15267  amgm2  15277  iseraltlem2  15590  iseraltlem3  15591  modfsummod  15701  binomlem  15736  binom11  15739  arisum  15767  arisum2  15768  pwdif  15775  georeclim  15779  geo2sum  15780  mertenslem1  15791  mertens  15793  prodfrec  15802  fprodm1s  15877  fprodp1s  15878  fprodmodd  15904  fallfacfwd  15943  0risefac  15945  bpolydiflem  15961  bpoly2  15964  bpoly3  15965  bpoly4  15966  fsumcube  15967  efzval  16011  resinval  16044  recosval  16045  efi4p  16046  tan0  16060  efival  16061  sinhval  16063  coshval  16064  cosadd  16074  cos2tsin  16088  ef01bndlem  16093  cos1bnd  16096  cos2bnd  16097  absefib  16107  efieq1re  16108  demoivreALT  16110  eirrlem  16113  rpnnen2lem3  16125  rpnnen2lem11  16133  ruclem7  16145  3dvds  16242  3dvdsdec  16243  3dvds2dec  16244  odd2np1  16252  nn0o1gt2  16292  nn0o  16294  pwp1fsum  16302  divalglem2  16306  divalglem9  16312  5ndvds3  16324  5ndvds6  16325  flodddiv4  16326  m1bits  16351  sadcp1  16366  sadeq  16383  smupp1  16391  smumul  16404  gcdaddmlem  16435  nn0expgcd  16475  3lcm2e6woprm  16526  nn0gcdsq  16663  phiprmpw  16687  prmdiv  16696  prmdiveq  16697  pythagtriplem1  16728  pythagtriplem12  16738  pythagtriplem14  16740  pockthi  16819  infpnlem1  16822  prmreclem4  16831  4sqlem12  16868  4sqlem13  16869  4sqlem19  16875  vdwapun  16886  vdwlem6  16898  0hashbc  16919  prmo2  16952  prmo3  16953  dec5dvds  16976  dec5nprm  16978  dec2nprm  16979  modxai  16980  modxp1i  16982  mod2xnegi  16983  modsubi  16984  gcdmodi  16986  decsplit0b  16991  decsplit1  16993  decsplit  16994  karatsuba  16995  2exp7  16999  2exp8  17000  3exp3  17003  5prm  17020  7prm  17022  11prm  17026  prmlem2  17031  37prm  17032  43prm  17033  83prm  17034  139prm  17035  163prm  17036  317prm  17037  631prm  17038  prmo5  17040  1259lem1  17042  1259lem2  17043  1259lem3  17044  1259lem4  17045  1259lem5  17046  2503lem1  17048  2503lem2  17049  2503lem3  17050  2503prm  17051  4001lem1  17052  4001lem2  17053  4001lem3  17054  4001lem4  17055  4001prm  17056  pwsbas  17391  rcaninv  17701  subsubc  17760  xpccatid  18094  chnub  18528  subsubmgm  18618  subsubm  18724  smndex2dnrinv  18823  mulg2  18996  subsubg  19062  oppgmnd  19266  gsumwrev  19278  psgnunilem2  19407  sylow1lem1  19510  subgslw  19528  sylow3  19545  efginvrel2  19639  efgsfo  19651  frgpnabllem1  19785  gsumzaddlem  19833  gsummptfzsplitl  19845  gsummpt1n0  19877  dprdfid  19931  ablfac1lem  19982  pgpfac1lem3  19991  pgpfaclem1  19995  ablsimpgfindlem1  20021  mgpress  20068  srgbinomlem4  20147  opprrng  20263  unitsubm  20304  subsubrng  20478  subsubrg  20513  cntzsdrg  20717  subdrgint  20718  lsslss  20894  xrsnsgrp  21344  gzrngunit  21370  expghm  21412  pzriprng1ALT  21433  chrid  21462  zrhpsgnmhm  21521  psgndiflemA  21538  frlmip  21715  frlmphl  21718  evlsval  22021  mpff  22039  coe1fzgsumdlem  22218  evl1gsumdlem  22271  matvsca2  22343  mattposvs  22370  m2detleiblem3  22544  m2detleiblem4  22545  cpmidpmat  22788  resstopn  23101  cnmpt1res  23591  ressuss  24177  iscusp2  24216  ucnextcn  24218  txmetcnp  24462  rerest  24719  xrtgioo  24722  xrrest  24723  cnmpopc  24849  xrhmeo  24871  clmvs2  25021  clmnegneg  25031  ncvsm1  25081  ncvspi  25083  cphassir  25142  cphipval2  25168  reust  25308  rrxprds  25316  csbren  25326  rrxdsfi  25338  minveclem2  25353  ovolunlem1a  25424  ovolicc2lem4  25448  uniioombllem5  25515  iblabs  25757  iblabsr  25758  iblmulc2  25759  itgmulc2  25762  limcres  25814  dvfval  25825  dvreslem  25837  dvres2lem  25838  dvcnp2  25848  dvcnp2OLD  25849  cpnres  25866  dvmulbr  25868  dvcobr  25876  dvcobrOLD  25877  dveflem  25910  lhop1lem  25945  lhop2  25947  dvcnvrelem2  25950  plyun0  26129  coeeulem  26156  coeeu  26157  dvply1  26218  dvtaylp  26305  taylthlem2  26309  taylthlem2OLD  26310  taylth  26311  dvradcnv  26357  pserdvlem2  26365  abelthlem8  26376  abelth  26378  sinhalfpilem  26399  cospi  26408  eulerid  26410  cos2pi  26412  ef2kpi  26414  sinhalfpip  26428  sinhalfpim  26429  coshalfpip  26430  coshalfpim  26431  sincosq3sgn  26436  sincosq4sgn  26437  tangtx  26441  sincos4thpi  26449  sincos6thpi  26452  sineq0  26460  tanregt0  26475  logm1  26525  abslogle  26554  tanarg  26555  logcnlem4  26581  advlogexp  26591  cxpsqrt  26639  dvsqrt  26678  dvcnsqrt  26680  cxpcn3  26685  root1cj  26693  cxpeq  26694  logb1  26706  2logb9irr  26732  sqrt2cxp2logb9e3  26736  ang180lem1  26746  ang180lem2  26747  ang180lem3  26748  lawcos  26753  isosctrlem1  26755  isosctrlem2  26756  quad2  26776  1cubrlem  26778  1cubr  26779  dcubic2  26781  mcubic  26784  binom4  26787  dquartlem1  26788  quart1lem  26792  quart1  26793  quartlem1  26794  asinlem  26805  asinlem2  26806  asinlem3a  26807  acosneg  26824  efiasin  26825  asinsinlem  26828  asinsin  26829  acoscos  26830  asin1  26831  acosbnd  26837  atancj  26847  efiatan  26849  atanlogaddlem  26850  efiatan2  26854  2efiatan  26855  tanatan  26856  cosatan  26858  atantan  26860  atanbndlem  26862  atans2  26868  dvatan  26872  atantayl  26874  atantayl2  26875  log2cnv  26881  log2tlbnd  26882  log2ublem2  26884  log2ublem3  26885  log2ub  26886  birthday  26891  jensenlem1  26924  amgmlem  26927  lgamgulmlem2  26967  lgamgulmlem5  26970  lgambdd  26974  ftalem2  27011  ftalem5  27014  ftalem6  27015  basellem2  27019  basellem3  27020  basellem5  27022  basellem8  27025  basellem9  27026  mule1  27085  ppi1i  27105  musum  27128  ppiublem1  27140  ppiub  27142  chtublem  27149  chtub  27150  dchrptlem1  27202  dchrptlem2  27203  bclbnd  27218  bposlem6  27227  bposlem8  27229  bposlem9  27230  lgsdir2lem1  27263  lgsdir2lem2  27264  lgsdir2lem4  27266  lgsdir2lem5  27267  lgsne0  27273  1lgs  27278  gausslemma2dlem0e  27298  gausslemma2dlem0f  27299  gausslemma2dlem3  27306  gausslemma2d  27312  lgseisenlem1  27313  lgseisenlem2  27314  lgseisenlem3  27315  lgseisenlem4  27316  lgseisen  27317  lgsquadlem1  27318  lgsquadlem2  27319  lgsquad2lem1  27322  lgsquad2lem2  27323  m1lgs  27326  2lgslem3a  27334  2lgslem3b  27335  2lgslem3c  27336  2lgslem3d  27337  2lgsoddprmlem3a  27348  2lgsoddprmlem3b  27349  2lgsoddprmlem3c  27350  2lgsoddprmlem3d  27351  addsqnreup  27381  chebbnd1lem2  27408  chebbnd1lem3  27409  rplogsumlem2  27423  dchrisum0flblem1  27446  dchrisum0re  27451  mulog2sumlem2  27473  chpdifbndlem1  27491  pntpbnd1a  27523  pntpbnd2  27525  pntibndlem2  27529  pntibndlem3  27530  pntlemg  27536  pntlemk  27544  pntlemo  27545  no2times  28340  zseo  28345  avgslt1d  28376  avgslt2d  28377  pw2cut2  28382  remulscllem1  28402  axsegconlem1  28895  ax5seglem7  28913  axlowdimlem3  28922  axlowdimlem16  28935  axlowdimlem17  28936  elntg2  28963  vdegp1bi  29516  vtxdginducedm1  29522  wlkp1lem1  29650  spthispth  29702  cyclnumvtx  29778  2wlkdlem1  29903  2pthd  29918  clwlkclwwlkfo  29989  3wlkdlem1  30139  3pthd  30154  eucrct2eupth  30225  numclwwlk5  30368  numclwwlk7  30371  frgrregord013  30375  ex-fl  30427  ex-mod  30429  ex-exp  30430  ex-bc  30432  ex-lcm  30438  ex-ind-dvds  30441  vc2OLD  30548  vc0  30554  vcm  30556  nvm1  30645  nvpi  30647  nvmtri  30651  nvge0  30653  ipval3  30689  ipidsq  30690  ip0i  30805  ip1ilem  30806  ip2i  30808  ipdirilem  30809  ipasslem10  30819  siilem1  30831  siii  30833  minvecolem2  30855  hvsubid  31006  hvaddsubval  31013  hvmul2negi  31028  hvadd12i  31037  hv2times  31041  hvnegdii  31042  hvaddcani  31045  hi01  31076  hisubcomi  31084  normlem0  31089  normlem1  31090  normlem3  31092  normlem9  31098  bcseqi  31100  normsqi  31112  norm-ii-i  31117  normsubi  31121  norm3difi  31127  norm3adifii  31128  normpar2i  31136  polid2i  31137  polidi  31138  chdmm2i  31458  chj12i  31502  spanunsni  31559  qlaxr5i  31615  osumcor2i  31624  spansnji  31626  pjadjii  31654  pjinormii  31656  pjsslem  31659  pjpythi  31702  mayete3i  31708  mayetes3i  31709  hoadd12i  31757  honegneg  31786  ho2times  31799  hoaddsubi  31801  hosd1i  31802  hosd2i  31803  honpncani  31807  lnopeq0lem1  31985  lnopunilem1  31990  lnophmlem2  31997  lnfn0i  32022  nmopcoadji  32081  nmopcoadj2i  32082  opsqrlem1  32120  opsqrlem5  32124  opsqrlem6  32125  pjclem3  32177  stadd3i  32228  mddmd2  32289  mdexchi  32315  cvexchlem  32348  atomli  32362  atordi  32364  atabs2i  32382  mdsymlem1  32383  iuninc  32540  suppss2f  32620  mptiffisupp  32674  suppss3  32706  binom2subadd  32725  pythagreim  32729  dfdec100  32813  dpfrac1  32872  decdiv10  32876  dpmul100  32877  dp3mul10  32878  dpmul1000  32879  dpexpp1  32888  dpadd2  32890  dpadd  32891  dpmul  32893  dpmul4  32894  threehalves  32895  1mhdrd  32896  pfxlsw2ccat  32931  ccatws1f1olast  32933  cyc2fv1  33090  cyc2fv2  33091  cycpmco2lem4  33098  cycpmco2lem5  33099  cyc3fv1  33106  cyc3fv2  33107  cyc3fv3  33108  archirngz  33158  gsumvsca2  33196  elrgspnlem4  33212  subsdrg  33264  nn0omnd  33309  nn0archi  33312  xrge0slmod  33313  opprabs  33447  ressply1evls1  33528  resssra  33599  lsssra  33600  fedgmullem1  33642  fedgmullem2  33643  fedgmul  33644  fldsdrgfldext2  33675  fldgenfldext  33681  fldextrspunlem1  33688  fldextrspunfld  33689  fldextrspundgdvdslem  33693  fldextrspundgdvds  33694  algextdeglem1  33730  algextdeglem4  33733  constrrtcclem  33747  constrmulcl  33784  constrinvcl  33786  2sqr3minply  33793  cos9thpiminplylem4  33798  cos9thpiminplylem5  33799  lmatfvlem  33828  sqsscirc1  33921  cnvordtrestixx  33926  raddcn  33942  xrge0iifhom  33950  xrge0mulc1cn  33954  xrge0tmd  33958  lmlimxrge0  33961  qqhucn  34005  rrhcn  34010  qqtopn  34024  rrhqima  34027  brfae  34261  inelcarsg  34324  cndprobnul  34450  isrrvv  34456  ballotlem1  34500  ballotlem2  34502  ballotlemi1  34516  ballotlemii  34517  ballotlemic  34520  ballotlem1c  34521  ballotlemfrceq  34542  ballotth  34551  ofcs2  34558  signsvtn0  34583  signstfveq0  34590  signsvtp  34596  signsvtn  34597  signsvfpn  34598  signsvfnn  34599  signshf  34601  hashreprin  34633  reprfz1  34637  chtvalz  34642  breprexp  34646  breprexpnat  34647  hgt750lemd  34661  hgt750lem  34664  hgt750lem2  34665  subfacp1lem1  35223  subfacp1lem5  35228  subfacp1lem6  35229  subfaclim  35232  cvmliftlem5  35333  cvmliftlem8  35336  cvmliftlem10  35338  cvmliftlem13  35340  cvmlift2lem6  35352  cvmlift2lem12  35358  problem1  35709  problem2  35710  problem4  35712  quad3  35714  iexpire  35779  itgeq12i  36250  sin2h  37660  poimirlem16  37686  poimirlem17  37687  poimirlem18  37688  poimirlem19  37689  poimirlem20  37690  poimirlem21  37691  poimirlem22  37692  poimirlem26  37696  mblfinlem3  37709  ismblfin  37711  itg2addnclem3  37723  iblabsnc  37734  iblmulc2nc  37735  itgmulc2nc  37738  ftc1cnnc  37742  ftc1anclem6  37748  ftc1anclem7  37749  ftc1anclem8  37750  dvasin  37754  fdc  37795  heiborlem4  37864  heiborlem6  37866  dalem24  39806  pmod2iN  39958  cdleme9  40362  cdleme20aN  40418  cdleme22e  40453  cdleme22eALTN  40454  cdleme25cv  40467  cdleme29b  40484  cdlemh1  40924  cdlemh2  40925  cdlemk35  41021  cdlemkid1  41031  12gcd5e1  42106  60gcd7e1  42108  420gcd8e4  42109  12lcm5e60  42111  420lcm8e840  42114  lcm1un  42116  lcm2un  42117  lcm3un  42118  lcm4un  42119  lcm5un  42120  lcm6un  42121  lcm7un  42122  lcm8un  42123  3factsumint1  42124  3factsumint3  42126  lcmineqlem10  42141  3exp7  42156  3lexlogpow5ineq1  42157  3lexlogpow5ineq5  42163  aks4d1p1  42179  5bc2eq10  42245  2ap1caineq  42248  aks5lem3a  42292  aks5lem7  42303  1p3e4  42362  sqmid3api  42386  sqn5i  42388  sqdeccom12  42392  235t711  42408  cxpi11d  42446  sin2t3rdpi  42456  cos2t3rdpi  42457  re1m1e0m0  42500  readdlid  42506  remul02  42508  sn-1ticom  42538  sn-mullid  42539  sn-0tie0  42554  sn-mul02  42555  sn-inelr  42590  mhphf2  42701  flt4lem5e  42759  sum9cubes  42775  pellexlem5  42936  reglog1  42999  jm2.23  43099  jm2.27c  43110  lnmlsslnm  43184  lmhmlnmsplit  43190  areaquad  43319  oaomoencom  43420  resqrtvalex  43748  imsqrtvalex  43749  cotrclrcl  43845  inductionexd  44258  hashnzfz2  44424  lhe4.4ex1a  44432  binomcxplemdvsum  44458  binomcxplemnotnn0  44459  binomcxp  44460  sineq0ALT  45039  unirnmapsn  45321  fzisoeu  45411  fsummulc1f  45681  fprodexp  45704  constlimc  45734  sumnnodd  45740  limcresiooub  45750  limcresioolb  45751  cncfshiftioo  46000  fperdvper  46027  dvnmul  46051  dvmptfprod  46053  itgsinexplem1  46062  stoweidlem11  46119  stoweidlem13  46121  stoweidlem26  46134  stoweidlem34  46142  wallispilem4  46176  wallispi2lem1  46179  wallispi2lem2  46180  stirlinglem11  46192  dirkerper  46204  dirkertrigeqlem1  46206  dirkertrigeqlem3  46208  dirkercncflem1  46211  dirkercncflem4  46214  fourierdlem30  46245  fourierdlem32  46247  fourierdlem33  46248  fourierdlem42  46257  fourierdlem46  46260  fourierdlem47  46261  fourierdlem57  46271  fourierdlem60  46274  fourierdlem61  46275  fourierdlem62  46276  fourierdlem68  46282  fourierdlem73  46287  fourierdlem79  46293  fourierdlem89  46303  fourierdlem90  46304  fourierdlem91  46305  fourierdlem96  46310  fourierdlem97  46311  fourierdlem98  46312  fourierdlem99  46313  fourierdlem100  46314  fourierdlem103  46317  fourierdlem104  46318  fourierdlem108  46322  fourierdlem110  46324  fourierdlem113  46327  sqwvfoura  46336  sqwvfourb  46337  fourierswlem  46338  fouriersw  46339  fouriercn  46340  etransclem4  46346  etransclem7  46349  etransclem23  46365  etransclem24  46366  etransclem25  46367  etransclem26  46368  etransclem31  46373  etransclem32  46374  etransclem35  46377  etransclem37  46379  etransclem46  46388  rrndistlt  46398  sge0tsms  46488  sge0xaddlem2  46542  vonioolem2  46789  ormklocald  46982  natlocalincr  46984  nthrucw  46994  1t10e1p1e11  47420  deccarry  47421  1fzopredsuc  47434  ceil5half3  47450  minusmodnep2tmod  47463  m1mod0mod1  47464  8mod5e3  47470  modmkpkne  47471  modm1p1ne  47480  iccpartgt  47537  fmtno0  47650  fmtno1  47651  fmtnorec2  47653  fmtno2  47660  fmtno3  47661  fmtno4  47662  fmtno5  47667  257prm  47671  fmtnofac1  47680  fmtno4prmfac  47682  fmtno4prmfac193  47683  fmtno4nprmfac193  47684  m2prm  47701  m3prm  47702  flsqrt5  47704  3ndvds4  47705  139prmALT  47706  31prm  47707  127prm  47709  m11nprm  47711  lighneallem2  47716  lighneallem3  47717  3exp4mod41  47726  41prothprmlem1  47727  41prothprmlem2  47728  41prothprm  47729  m1expevenALTV  47757  1oddALTV  47800  6even  47821  8even  47823  2exp340mod341  47843  341fppr2  47844  4fppr1  47845  8exp8mod9  47846  9fppr8  47847  nfermltl8rev  47852  gbpart7  47877  gbpart9  47879  gbpart11  47880  sbgoldbo  47897  bgoldbtbndlem1  47915  tgoldbachlt  47926  gpg3kgrtriexlem2  48194  gpg3kgrtriexlem4  48196  gpg3kgrtriexlem6  48198  gpg3kgrtriex  48199  gpgprismgr4cycllem3  48207  gpgprismgr4cycllem11  48215  pgnbgreunbgrlem2lem1  48224  pgnbgreunbgrlem2lem2  48225  pgnbgreunbgrlem4  48229  pgnbgreunbgrlem5lem1  48230  pgnbgreunbgrlem5lem2  48231  gpg5edgnedg  48240  altgsumbcALT  48463  lincfsuppcl  48524  linccl  48525  lincvalsn  48528  lincdifsn  48535  lincsum  48540  lincscm  48541  lindslinindimp2lem4  48572  lindslinindsimp2lem5  48573  snlindsntor  48582  lincresunit3lem2  48591  zlmodzxzldeplem3  48613  ldepsnlinc  48619  nn0sumshdiglemA  48730  nn0sumshdiglemB  48731  ackval2  48793  ackval2012  48802  ackval3012  48803  ackval41a  48805  ackval42  48807  ackval42a  48808  affinecomb1  48813  rrx2linest  48853  itschlc0yqe  48871  itsclc0yqsollem1  48873  itscnhlc0xyqsol  48876  itschlc0xyqsol1  48877  itsclquadb  48887  2itscplem2  48890  itscnhlinecirc02plem2  48894  oppcup  49318  natoppf  49340  islmd  49776  iscmd  49777  lmddu  49778  sinh-conventional  49850  onetansqsecsq  49872  cotsqcscsq  49873  mvlraddi  49882  mvlrmuli  49888  amgmwlem  49913  amgmlemALT  49914