Theorem mulassd 9548

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 9509	. 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 1226	1 |- ( ph -> ( ( A x. B ) x. C ) = ( A x. ( B x. C ) ) )

Syntax hints:   -> wi 4   = wceq 1399   e. wcel 1836  (class class class)co 6214   CCcc 9419   x. cmul 9426

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

This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 973

This theorem is referenced by:  recex  10116  mulcand  10117  receu  10129  divdivdiv  10180  divmuleq  10184  conjmul  10196  modmul1  11962  moddi  11976  expadd  12130  binom3  12208  digit1  12221  discr1  12223  discr  12224  faclbnd  12289  faclbnd6  12298  bcm1k  12314  bcp1nk  12316  crre  12968  remullem  12982  amgm2  13223  iseraltlem2  13526  iseraltlem3  13527  binomlem  13662  climcndslem2  13683  geo2sum  13703  mertenslem1  13714  clim2prod  13718  sinadd  13920  tanadd  13923  bezoutlem3  14199  dvdsmulgcd  14213  qredeq  14268  pcaddlem  14428  prmpwdvds  14443  ablfacrp  17249  nmoco  21348  cph2ass  21763  csbren  21930  minveclem2  21945  uniioombllem5  22100  itg1mulc  22215  mbfi1fseqlem5  22230  itgconst  22329  itgmulc2  22344  dvexp  22460  dvply1  22784  elqaalem3  22821  aalioulem1  22832  aaliou3lem2  22843  dvtaylp  22869  dvradcnv  22920  pserdvlem2  22927  tangtx  23002  tanregt0  23030  tanarg  23110  logcnlem4  23132  cxpmul  23175  dvcxp1  23222  root1eq1  23235  heron  23304  quad2  23305  dcubic1lem  23309  dcubic1  23311  cubic2  23314  binom4  23316  dquartlem1  23317  dquartlem2  23318  dquart  23319  quart1lem  23321  quart1  23322  quartlem1  23323  efiasin  23354  asinsinlem  23357  asinsin  23358  efiatan  23378  efiatan2  23383  2efiatan  23384  atantan  23389  atanbndlem  23391  atans2  23397  atantayl  23403  log2cnv  23410  log2tlbnd  23411  ftalem1  23482  ftalem5  23486  basellem3  23492  basellem5  23494  basellem8  23497  chtub  23623  perfectlem1  23640  perfectlem2  23641  perfect  23642  bcmono  23688  bclbnd  23691  bposlem9  23703  lgsneg  23730  lgseisenlem1  23760  lgseisenlem2  23761  lgseisenlem3  23762  lgseisenlem4  23763  lgsquad2lem1  23769  lgsquad3  23772  2sqlem3  23777  chto1ub  23797  rplogsumlem1  23805  dchrmusum2  23815  dchrvmasum2lem  23817  dchrvmasumlem2  23819  dchrvmasumiflem2  23823  dchrisum0lem1  23837  dchrisum0lem2  23839  mulog2sumlem2  23856  chpdifbndlem1  23874  selberg3lem1  23878  selberg4lem1  23881  selberg34r  23892  pntrlog2bndlem3  23900  pntrlog2bndlem5  23902  pntrlog2bndlem6  23904  pntlemh  23920  pntlemr  23923  pntlemf  23926  pntlemk  23927  pntlemo  23928  colinearalglem4  24354  axpasch  24386  axcontlem2  24410  axcontlem4  24412  axcontlem7  24415  axcontlem8  24416  ipasslem4  25887  minvecolem2  25929  his35  26143  leopnmid  27194  oddpwdc  28512  subfacval2  28856  subfaclim  28857  circum  29265  fallrisefac  29349  binomfallfaclem2  29364  faclimlem1  29370  faclimlem3  29372  faclim2  29375  bpolydiflem  30005  bpoly4  30010  itgmulc2nc  30285  dvcncxp1  30302  areacirclem1  30309  areacirclem4  30312  bfplem1  30520  pellexlem6  30971  rmxluc  31073  rmyluc2  31075  rmydbl  31077  jm2.18  31132  jm2.23  31140  jm2.27c  31151  jm3.1lem2  31162  proot1ex  31365  binomcxplemnotnn0  31465  mul13d  31663  fmul01lt1lem1  31779  fmul01lt1lem2  31780  coskpi2  31867  cosknegpi  31870  dvnxpaek  31940  dvmptfprodlem  31942  dvnprodlem2  31945  itgsinexplem1  31953  stoweidlem26  32009  wallispilem5  32052  wallispi  32053  wallispi2lem1  32054  wallispi2lem2  32055  stirlinglem3  32059  stirlinglem10  32066  stirlinglem15  32071  dirkertrigeqlem1  32081  dirkertrigeqlem2  32082  dirkertrigeqlem3  32083  dirkertrigeq  32084  dirkercncflem2  32087  fourierdlem66  32156  fourierswlem  32214  fouriersw  32215  etransclem23  32241  etransclem25  32243  etransclem46  32264  sigarls  32275  sharhght  32283  perfectALTVlem1  32578  perfectALTVlem2  32579  perfectALTV  32580  2zrngmmgm  32987  altgsumbcALT  33177  nn0sumshdiglemB  33476  aacllem  33585  int-mulassocd  38562