Theorem mulassd 9622

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

Syntax hints:   -> wi 4   = wceq 1383   e. wcel 1804  (class class class)co 6281   CCcc 9493   x. cmul 9500

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

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976

This theorem is referenced by:  recex  10188  mulcand  10189  receu  10201  divdivdiv  10252  divmuleq  10256  conjmul  10268  modmul1  12022  moddi  12036  expadd  12190  binom3  12269  digit1  12282  discr1  12284  discr  12285  faclbnd  12350  faclbnd6  12359  bcm1k  12375  bcp1nk  12377  crre  12929  remullem  12943  amgm2  13184  iseraltlem2  13487  iseraltlem3  13488  binomlem  13623  climcndslem2  13644  geo2sum  13664  mertenslem1  13675  clim2prod  13679  sinadd  13881  tanadd  13884  bezoutlem3  14160  dvdsmulgcd  14174  qredeq  14229  pcaddlem  14389  prmpwdvds  14404  ablfacrp  17096  nmoco  21222  cph2ass  21637  csbren  21804  minveclem2  21819  uniioombllem5  21974  itg1mulc  22089  mbfi1fseqlem5  22104  itgconst  22203  itgmulc2  22218  dvexp  22334  dvply1  22658  elqaalem3  22695  aalioulem1  22706  aaliou3lem2  22717  dvtaylp  22743  dvradcnv  22794  pserdvlem2  22801  tangtx  22876  tanregt0  22904  tanarg  22982  logcnlem4  23004  cxpmul  23047  dvcxp1  23094  root1eq1  23107  heron  23147  quad2  23148  dcubic1lem  23152  dcubic1  23154  cubic2  23157  binom4  23159  dquartlem1  23160  dquartlem2  23161  dquart  23162  quart1lem  23164  quart1  23165  quartlem1  23166  efiasin  23197  asinsinlem  23200  asinsin  23201  efiatan  23221  efiatan2  23226  2efiatan  23227  atantan  23232  atanbndlem  23234  atans2  23240  atantayl  23246  log2cnv  23253  log2tlbnd  23254  ftalem1  23324  ftalem5  23328  basellem3  23334  basellem5  23336  basellem8  23339  chtub  23465  perfectlem1  23482  perfectlem2  23483  perfect  23484  bcmono  23530  bclbnd  23533  bposlem9  23545  lgsneg  23572  lgseisenlem1  23602  lgseisenlem2  23603  lgseisenlem3  23604  lgseisenlem4  23605  lgsquad2lem1  23611  lgsquad3  23614  2sqlem3  23619  chto1ub  23639  rplogsumlem1  23647  dchrmusum2  23657  dchrvmasum2lem  23659  dchrvmasumlem2  23661  dchrvmasumiflem2  23665  dchrisum0lem1  23679  dchrisum0lem2  23681  mulog2sumlem2  23698  chpdifbndlem1  23716  selberg3lem1  23720  selberg4lem1  23723  selberg34r  23734  pntrlog2bndlem3  23742  pntrlog2bndlem5  23744  pntrlog2bndlem6  23746  pntlemh  23762  pntlemr  23765  pntlemf  23768  pntlemk  23769  pntlemo  23770  colinearalglem4  24190  axpasch  24222  axcontlem2  24246  axcontlem4  24248  axcontlem7  24251  axcontlem8  24252  ipasslem4  25727  minvecolem2  25769  his35  25983  leopnmid  27035  oddpwdc  28271  subfacval2  28609  subfaclim  28610  circum  29018  fallrisefac  29123  binomfallfaclem2  29138  faclimlem1  29144  faclimlem3  29146  faclim2  29149  bpolydiflem  29792  bpoly4  29797  itgmulc2nc  30059  dvcncxp1  30076  areacirclem1  30083  areacirclem4  30086  bfplem1  30294  pellexlem6  30746  rmxluc  30848  rmyluc2  30850  rmydbl  30852  jm2.18  30906  jm2.23  30914  jm2.27c  30925  jm3.1lem2  30936  proot1ex  31137  mul13d  31415  fmul01lt1lem1  31532  fmul01lt1lem2  31533  coskpi2  31620  cosknegpi  31623  dvnxpaek  31693  dvmptfprodlem  31695  dvnprodlem2  31698  itgsinexplem1  31706  stoweidlem26  31762  wallispilem5  31805  wallispi  31806  wallispi2lem1  31807  wallispi2lem2  31808  stirlinglem3  31812  stirlinglem10  31819  stirlinglem15  31824  dirkertrigeqlem1  31834  dirkertrigeqlem2  31835  dirkertrigeqlem3  31836  dirkertrigeq  31837  dirkercncflem2  31840  fourierdlem66  31909  fourierswlem  31967  fouriersw  31968  etransclem23  31994  etransclem25  31996  etransclem46  32017  sigarls  32028  sharhght  32036  2zrngmmgm  32579  altgsumbcALT  32810