Theorem mulassd 9665

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 9626	. 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 1870  (class class class)co 6305   CCcc 9536   x. cmul 9543

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

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

This theorem is referenced by:  recex  10243  mulcand  10244  receu  10256  divdivdiv  10307  divmuleq  10311  conjmul  10323  modmul1  12140  moddi  12154  expadd  12311  binom3  12390  digit1  12403  discr1  12405  discr  12406  faclbnd  12472  faclbnd6  12481  bcm1k  12497  bcp1nk  12499  crre  13156  remullem  13170  amgm2  13411  iseraltlem2  13727  iseraltlem3  13728  binomlem  13865  climcndslem2  13886  geo2sum  13907  mertenslem1  13918  clim2prod  13922  fallrisefac  14056  binomfallfaclem2  14071  bpolydiflem  14085  bpoly4  14090  sinadd  14196  tanadd  14199  bezoutlem3  14479  dvdsmulgcd  14493  qredeq  14634  pcaddlem  14796  prmpwdvds  14811  ablfacrp  17634  nmoco  21669  cph2ass  22083  csbren  22246  minveclem2  22261  uniioombllem5  22422  itg1mulc  22539  mbfi1fseqlem5  22554  itgconst  22653  itgmulc2  22668  dvexp  22784  dvply1  23105  elqaalem3  23142  aalioulem1  23153  aaliou3lem2  23164  dvtaylp  23190  dvradcnv  23241  pserdvlem2  23248  tangtx  23325  tanregt0  23353  tanarg  23433  logcnlem4  23455  cxpmul  23498  dvcxp1  23545  dvcncxp1  23548  root1eq1  23560  heron  23629  quad2  23630  dcubic1lem  23634  dcubic1  23636  cubic2  23639  binom4  23641  dquartlem1  23642  dquartlem2  23643  dquart  23644  quart1lem  23646  quart1  23647  quartlem1  23648  efiasin  23679  asinsinlem  23682  asinsin  23683  efiatan  23703  efiatan2  23708  2efiatan  23709  atantan  23714  atanbndlem  23716  atans2  23722  atantayl  23728  log2cnv  23735  log2tlbnd  23736  ftalem1  23862  ftalem5  23866  basellem3  23872  basellem5  23874  basellem8  23877  chtub  24003  perfectlem1  24020  perfectlem2  24021  perfect  24022  bcmono  24068  bclbnd  24071  bposlem9  24083  lgsneg  24110  lgseisenlem1  24140  lgseisenlem2  24141  lgseisenlem3  24142  lgseisenlem4  24143  lgsquad2lem1  24149  lgsquad3  24152  2sqlem3  24157  chto1ub  24177  rplogsumlem1  24185  dchrmusum2  24195  dchrvmasum2lem  24197  dchrvmasumlem2  24199  dchrvmasumiflem2  24203  dchrisum0lem1  24217  dchrisum0lem2  24219  mulog2sumlem2  24236  chpdifbndlem1  24254  selberg3lem1  24258  selberg4lem1  24261  selberg34r  24272  pntrlog2bndlem3  24280  pntrlog2bndlem5  24282  pntrlog2bndlem6  24284  pntlemh  24300  pntlemr  24303  pntlemf  24306  pntlemk  24307  pntlemo  24308  colinearalglem4  24785  axpasch  24817  axcontlem2  24841  axcontlem4  24843  axcontlem7  24846  axcontlem8  24847  ipasslem4  26320  minvecolem2  26362  his35  26576  leopnmid  27626  oddpwdc  29013  subfacval2  29698  subfaclim  29699  circum  30106  faclimlem1  30166  faclimlem3  30168  faclim2  30171  itgmulc2nc  31713  areacirclem1  31735  areacirclem4  31738  bfplem1  31857  pellexlem6  35387  rmxluc  35489  rmyluc2  35491  rmydbl  35493  jm2.18  35548  jm2.23  35556  jm2.27c  35567  jm3.1lem2  35578  proot1ex  35776  int-mulassocd  36260  binomcxplemnotnn0  36341  mul13d  37097  fmul01lt1lem1  37233  fmul01lt1lem2  37234  coskpi2  37312  cosknegpi  37315  dvnxpaek  37385  dvmptfprodlem  37387  dvnprodlem2  37390  itgsinexplem1  37398  stoweidlem26  37454  wallispilem5  37499  wallispi  37500  wallispi2lem1  37501  wallispi2lem2  37502  stirlinglem3  37506  stirlinglem10  37513  stirlinglem15  37518  dirkertrigeqlem1  37528  dirkertrigeqlem2  37529  dirkertrigeqlem3  37530  dirkertrigeq  37531  dirkercncflem2  37534  fourierdlem66  37603  fourierswlem  37661  fouriersw  37662  etransclem23  37688  etransclem25  37690  etransclem46  37711  sigarls  37865  sharhght  37873  perfectALTVlem1  38232  perfectALTVlem2  38233  perfectALTV  38234  2zrngmmgm  38703  altgsumbcALT  38893  nn0sumshdiglemB  39191  aacllem  39300