Theorem mulassd 9067

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

Syntax hints:   -> wi 4   = wceq 1649   e. wcel 1721  (class class class)co 6040   CCcc 8944   x. cmul 8951

This theorem is referenced by:  recex  9610  mulcand  9611  receu  9623  divdivdiv  9671  divmuleq  9675  conjmul  9687  modmul1  11234  moddi  11239  expadd  11377  binom3  11455  digit1  11468  discr1  11470  discr  11471  faclbnd  11536  faclbnd6  11545  bcm1k  11561  bcp1nk  11563  crre  11874  remullem  11888  amgm2  12128  iseraltlem2  12431  iseraltlem3  12432  binomlem  12563  climcndslem2  12585  geo2sum  12605  mertenslem1  12616  sinadd  12720  tanadd  12723  bezoutlem3  12995  dvdsmulgcd  13009  qredeq  13061  pcaddlem  13212  prmpwdvds  13227  ablfacrp  15579  nmoco  18724  cph2ass  19128  minveclem2  19280  uniioombllem5  19432  itg1mulc  19549  mbfi1fseqlem5  19564  itgconst  19663  itgmulc2  19678  dvexp  19792  dvply1  20154  elqaalem3  20191  aalioulem1  20202  aaliou3lem2  20213  dvtaylp  20239  dvradcnv  20290  pserdvlem2  20297  tangtx  20366  tanregt0  20394  tanarg  20467  logcnlem4  20489  cxpmul  20532  dvcxp1  20579  root1eq1  20592  quad2  20632  dcubic1lem  20636  dcubic1  20638  cubic2  20641  binom4  20643  dquartlem1  20644  dquartlem2  20645  dquart  20646  quart1lem  20648  quart1  20649  quartlem1  20650  efiasin  20681  asinsinlem  20684  asinsin  20685  efiatan  20705  efiatan2  20710  2efiatan  20711  atantan  20716  atanbndlem  20718  atans2  20724  atantayl  20730  log2cnv  20737  log2tlbnd  20738  ftalem1  20808  ftalem5  20812  basellem3  20818  basellem5  20820  basellem8  20823  chtub  20949  perfectlem1  20966  perfectlem2  20967  perfect  20968  bcmono  21014  bclbnd  21017  bposlem9  21029  lgsneg  21056  lgseisenlem1  21086  lgseisenlem2  21087  lgseisenlem3  21088  lgseisenlem4  21089  lgsquad2lem1  21095  lgsquad3  21098  2sqlem3  21103  chto1ub  21123  rplogsumlem1  21131  dchrmusum2  21141  dchrvmasum2lem  21143  dchrvmasumlem2  21145  dchrvmasumiflem2  21149  dchrisum0lem1  21163  dchrisum0lem2  21165  mulog2sumlem2  21182  chpdifbndlem1  21200  selberg3lem1  21204  selberg4lem1  21207  selberg34r  21218  pntrlog2bndlem3  21226  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  pntlemh  21246  pntlemr  21249  pntlemf  21252  pntlemk  21253  pntlemo  21254  ipasslem4  22288  minvecolem2  22330  his35  22543  leopnmid  23594  subfacval2  24826  subfaclim  24827  circum  25064  clim2prod  25169  fallrisefac  25293  binomfallfaclem2  25307  faclimlem1  25310  faclimlem3  25312  faclim2  25315  colinearalglem4  25752  axpasch  25784  axcontlem2  25808  axcontlem4  25810  axcontlem7  25813  axcontlem8  25814  bpolydiflem  26004  bpoly4  26009  itgmulc2nc  26172  dvreasin  26179  areacirclem2  26181  areacirclem5  26185  csbrn  26346  bfplem1  26421  pellexlem6  26787  rmxluc  26889  rmyluc2  26891  rmydbl  26893  jm2.18  26949  jm2.23  26957  jm2.27c  26968  jm3.1lem2  26979  proot1ex  27388  fmul01lt1lem1  27581  fmul01lt1lem2  27582  itgsinexplem1  27615  stoweidlem26  27642  wallispilem5  27685  wallispi  27686  wallispi2lem1  27687  wallispi2lem2  27688  stirlinglem3  27692  stirlinglem10  27699  stirlinglem15  27704  sigarls  27714  sharhght  27722

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

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938