Theorem mulassd 9617

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

Syntax hints:   -> wi 4   = wceq 1437   e. wcel 1872  (class class class)co 6249   CCcc 9488   x. cmul 9495

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

This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984

This theorem is referenced by:  recex  10195  mulcand  10196  receu  10208  divdivdiv  10259  divmuleq  10263  conjmul  10275  modmul1  12093  moddi  12107  expadd  12264  binom3  12343  digit1  12356  discr1  12358  discr  12359  faclbnd  12425  faclbnd6  12434  bcm1k  12450  bcp1nk  12452  crre  13121  remullem  13135  amgm2  13376  iseraltlem2  13692  iseraltlem3  13693  binomlem  13830  climcndslem2  13851  geo2sum  13872  mertenslem1  13883  clim2prod  13887  fallrisefac  14021  binomfallfaclem2  14036  bpolydiflem  14050  bpoly4  14055  sinadd  14161  tanadd  14164  bezoutlem3OLD  14448  bezoutlem3  14451  dvdsmulgcd  14465  qredeq  14606  pcaddlem  14776  prmpwdvds  14791  ablfacrp  17642  nmoco  21700  cph2ass  22132  csbren  22295  minveclem2  22310  minveclem2OLD  22322  uniioombllem5  22487  itg1mulc  22604  mbfi1fseqlem5  22619  itgconst  22718  itgmulc2  22733  dvexp  22849  dvply1  23179  elqaalem3  23216  elqaalem3OLD  23219  aalioulem1  23230  aaliou3lem2  23241  dvtaylp  23267  dvradcnv  23318  pserdvlem2  23325  tangtx  23402  tanregt0  23430  tanarg  23510  logcnlem4  23532  cxpmul  23575  dvcxp1  23622  dvcncxp1  23625  root1eq1  23637  heron  23706  quad2  23707  dcubic1lem  23711  dcubic1  23713  cubic2  23716  binom4  23718  dquartlem1  23719  dquartlem2  23720  dquart  23721  quart1lem  23723  quart1  23724  quartlem1  23725  efiasin  23756  asinsinlem  23759  asinsin  23760  efiatan  23780  efiatan2  23785  2efiatan  23786  atantan  23791  atanbndlem  23793  atans2  23799  atantayl  23805  log2cnv  23812  log2tlbnd  23813  ftalem1  23939  ftalem5  23943  ftalem5OLD  23945  basellem3  23951  basellem5  23953  basellem8  23956  chtub  24082  perfectlem1  24099  perfectlem2  24100  perfect  24101  bcmono  24147  bclbnd  24150  bposlem9  24162  lgsneg  24189  lgseisenlem1  24219  lgseisenlem2  24220  lgseisenlem3  24221  lgseisenlem4  24222  lgsquad2lem1  24228  lgsquad3  24231  2sqlem3  24236  chto1ub  24256  rplogsumlem1  24264  dchrmusum2  24274  dchrvmasum2lem  24276  dchrvmasumlem2  24278  dchrvmasumiflem2  24282  dchrisum0lem1  24296  dchrisum0lem2  24298  mulog2sumlem2  24315  chpdifbndlem1  24333  selberg3lem1  24337  selberg4lem1  24340  selberg34r  24351  pntrlog2bndlem3  24359  pntrlog2bndlem5  24361  pntrlog2bndlem6  24363  pntlemh  24379  pntlemr  24382  pntlemf  24385  pntlemk  24386  pntlemo  24387  colinearalglem4  24881  axpasch  24913  axcontlem2  24937  axcontlem4  24939  axcontlem7  24942  axcontlem8  24943  ipasslem4  26417  minvecolem2  26459  minvecolem2OLD  26469  his35  26683  leopnmid  27733  oddpwdc  29139  subfacval2  29862  subfaclim  29863  circum  30270  faclimlem1  30330  faclimlem3  30332  faclim2  30335  itgmulc2nc  31917  areacirclem1  31939  areacirclem4  31942  bfplem1  32061  pellexlem6  35591  rmxluc  35697  rmyluc2  35699  rmydbl  35701  jm2.18  35756  jm2.23  35764  jm2.27c  35775  jm3.1lem2  35786  proot1ex  35991  int-mulassocd  36537  binomcxplemnotnn0  36618  mul13d  37386  fmul01lt1lem1  37545  fmul01lt1lem2  37546  coskpi2  37624  cosknegpi  37627  dvnxpaek  37700  dvmptfprodlem  37702  dvnprodlem2  37705  itgsinexplem1  37713  stoweidlem26  37769  wallispilem5  37814  wallispi  37815  wallispi2lem1  37816  wallispi2lem2  37817  stirlinglem3  37821  stirlinglem10  37828  stirlinglem15  37833  dirkertrigeqlem1  37843  dirkertrigeqlem2  37844  dirkertrigeqlem3  37845  dirkertrigeq  37846  dirkercncflem2  37849  fourierdlem66  37919  fourierswlem  37977  fouriersw  37978  etransclem23  38005  etransclem25  38007  etransclem46  38028  hoidmvlelem2  38265  sigarls  38280  sharhght  38288  perfectALTVlem1  38656  perfectALTVlem2  38657  perfectALTV  38658  2zrngmmgm  39547  altgsumbcALT  39737  nn0sumshdiglemB  40034  aacllem  40143