Theorem mulassd 9691

Description: Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	|- ( ph -> A e. CC )
addcld.2	|- ( ph -> B e. CC )
addassd.3	|- ( ph -> C e. CC )

Assertion

Ref	Expression
mulassd	|- ( ph -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )

Proof of Theorem mulassd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 |- ( ph -> A e. CC )
2		addcld.2	. 2 |- ( ph -> B e. CC )
3		addassd.3	. 2 |- ( ph -> C e. CC )
4		mulass 9652	. 2 |- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )
5	1, 2, 3, 4	syl3anc 1276	1 |- ( ph -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )

Syntax hints:   -> wi 4   = wceq 1454   e. wcel 1897  (class class class)co 6314   CCcc 9562   x. cmul 9569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 9630

This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993

This theorem is referenced by:  recex  10271  mulcand  10272  receu  10284  divdivdiv  10335  divmuleq  10339  conjmul  10351  modmul1  12174  moddi  12188  expadd  12345  binom3  12424  digit1  12437  discr1  12439  discr  12440  faclbnd  12506  faclbnd6  12515  bcm1k  12531  bcp1nk  12533  crre  13225  remullem  13239  amgm2  13480  iseraltlem2  13797  iseraltlem3  13798  binomlem  13935  climcndslem2  13956  geo2sum  13977  mertenslem1  13988  clim2prod  13992  fallrisefac  14126  binomfallfaclem2  14141  bpolydiflem  14155  bpoly4  14160  sinadd  14266  tanadd  14269  bezoutlem3OLD  14553  bezoutlem3  14556  dvdsmulgcd  14570  qredeq  14711  pcaddlem  14881  prmpwdvds  14896  ablfacrp  17747  nmoco  21806  cph2ass  22238  csbren  22401  minveclem2  22416  minveclem2OLD  22428  uniioombllem5  22593  itg1mulc  22710  mbfi1fseqlem5  22725  itgconst  22824  itgmulc2  22839  dvexp  22955  dvply1  23285  elqaalem3  23322  elqaalem3OLD  23325  aalioulem1  23336  aaliou3lem2  23347  dvtaylp  23373  dvradcnv  23424  pserdvlem2  23431  tangtx  23508  tanregt0  23536  tanarg  23616  logcnlem4  23638  cxpmul  23681  dvcxp1  23728  dvcncxp1  23731  root1eq1  23743  heron  23812  quad2  23813  dcubic1lem  23817  dcubic1  23819  cubic2  23822  binom4  23824  dquartlem1  23825  dquartlem2  23826  dquart  23827  quart1lem  23829  quart1  23830  quartlem1  23831  efiasin  23862  asinsinlem  23865  asinsin  23866  efiatan  23886  efiatan2  23891  2efiatan  23892  atantan  23897  atanbndlem  23899  atans2  23905  atantayl  23911  log2cnv  23918  log2tlbnd  23919  ftalem1  24045  ftalem5  24049  ftalem5OLD  24051  basellem3  24057  basellem5  24059  basellem8  24062  chtub  24188  perfectlem1  24205  perfectlem2  24206  perfect  24207  bcmono  24253  bclbnd  24256  bposlem9  24268  lgsneg  24295  lgseisenlem1  24325  lgseisenlem2  24326  lgseisenlem3  24327  lgseisenlem4  24328  lgsquad2lem1  24334  lgsquad3  24337  2sqlem3  24342  chto1ub  24362  rplogsumlem1  24370  dchrmusum2  24380  dchrvmasum2lem  24382  dchrvmasumlem2  24384  dchrvmasumiflem2  24388  dchrisum0lem1  24402  dchrisum0lem2  24404  mulog2sumlem2  24421  chpdifbndlem1  24439  selberg3lem1  24443  selberg4lem1  24446  selberg34r  24457  pntrlog2bndlem3  24465  pntrlog2bndlem5  24467  pntrlog2bndlem6  24469  pntlemh  24485  pntlemr  24488  pntlemf  24491  pntlemk  24492  pntlemo  24493  colinearalglem4  24987  axpasch  25019  axcontlem2  25043  axcontlem4  25045  axcontlem7  25048  axcontlem8  25049  ipasslem4  26523  minvecolem2  26565  minvecolem2OLD  26575  his35  26789  leopnmid  27839  oddpwdc  29235  subfacval2  29958  subfaclim  29959  circum  30366  faclimlem1  30427  faclimlem3  30429  faclim2  30432  itgmulc2nc  32054  areacirclem1  32076  areacirclem4  32079  bfplem1  32198  pellexlem6  35722  rmxluc  35828  rmyluc2  35830  rmydbl  35832  jm2.18  35887  jm2.23  35895  jm2.27c  35906  jm3.1lem2  35917  proot1ex  36122  int-mulassocd  36667  binomcxplemnotnn0  36748  mul13d  37526  fmul01lt1lem1  37699  fmul01lt1lem2  37700  coskpi2  37778  cosknegpi  37781  dvnxpaek  37854  dvmptfprodlem  37856  dvnprodlem2  37859  itgsinexplem1  37867  stoweidlem26  37923  wallispilem5  37968  wallispi  37969  wallispi2lem1  37970  wallispi2lem2  37971  stirlinglem3  37975  stirlinglem10  37982  stirlinglem15  37987  dirkertrigeqlem1  37997  dirkertrigeqlem2  37998  dirkertrigeqlem3  37999  dirkertrigeq  38000  dirkercncflem2  38003  fourierdlem66  38073  fourierswlem  38131  fouriersw  38132  etransclem23  38159  etransclem25  38161  etransclem46  38182  hoidmvlelem2  38455  sigarls  38503  sharhght  38511  perfectALTVlem1  38880  perfectALTVlem2  38881  perfectALTV  38882  2zrngmmgm  40218  altgsumbcALT  40406  nn0sumshdiglemB  40703  aacllem  40812