Theorem mulassd 9521

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

Syntax hints:   -> wi 4   = wceq 1370   e. wcel 1758  (class class class)co 6201   CCcc 9392   x. cmul 9399

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

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

This theorem is referenced by:  recex  10080  mulcand  10081  receu  10093  divdivdiv  10144  divmuleq  10148  conjmul  10160  modmul1  11870  moddi  11884  expadd  12024  binom3  12103  digit1  12116  discr1  12118  discr  12119  faclbnd  12184  faclbnd6  12193  bcm1k  12209  bcp1nk  12211  crre  12722  remullem  12736  amgm2  12976  iseraltlem2  13279  iseraltlem3  13280  binomlem  13411  climcndslem2  13432  geo2sum  13452  mertenslem1  13463  sinadd  13567  tanadd  13570  bezoutlem3  13843  dvdsmulgcd  13857  qredeq  13911  pcaddlem  14069  prmpwdvds  14084  ablfacrp  16690  nmoco  20449  cph2ass  20864  csbren  21031  minveclem2  21046  uniioombllem5  21201  itg1mulc  21316  mbfi1fseqlem5  21331  itgconst  21430  itgmulc2  21445  dvexp  21561  dvply1  21884  elqaalem3  21921  aalioulem1  21932  aaliou3lem2  21943  dvtaylp  21969  dvradcnv  22020  pserdvlem2  22027  tangtx  22101  tanregt0  22129  tanarg  22202  logcnlem4  22224  cxpmul  22267  dvcxp1  22314  root1eq1  22327  heron  22367  quad2  22368  dcubic1lem  22372  dcubic1  22374  cubic2  22377  binom4  22379  dquartlem1  22380  dquartlem2  22381  dquart  22382  quart1lem  22384  quart1  22385  quartlem1  22386  efiasin  22417  asinsinlem  22420  asinsin  22421  efiatan  22441  efiatan2  22446  2efiatan  22447  atantan  22452  atanbndlem  22454  atans2  22460  atantayl  22466  log2cnv  22473  log2tlbnd  22474  ftalem1  22544  ftalem5  22548  basellem3  22554  basellem5  22556  basellem8  22559  chtub  22685  perfectlem1  22702  perfectlem2  22703  perfect  22704  bcmono  22750  bclbnd  22753  bposlem9  22765  lgsneg  22792  lgseisenlem1  22822  lgseisenlem2  22823  lgseisenlem3  22824  lgseisenlem4  22825  lgsquad2lem1  22831  lgsquad3  22834  2sqlem3  22839  chto1ub  22859  rplogsumlem1  22867  dchrmusum2  22877  dchrvmasum2lem  22879  dchrvmasumlem2  22881  dchrvmasumiflem2  22885  dchrisum0lem1  22899  dchrisum0lem2  22901  mulog2sumlem2  22918  chpdifbndlem1  22936  selberg3lem1  22940  selberg4lem1  22943  selberg34r  22954  pntrlog2bndlem3  22962  pntrlog2bndlem5  22964  pntrlog2bndlem6  22966  pntlemh  22982  pntlemr  22985  pntlemf  22988  pntlemk  22989  pntlemo  22990  colinearalglem4  23308  axpasch  23340  axcontlem2  23364  axcontlem4  23366  axcontlem7  23369  axcontlem8  23370  ipasslem4  24387  minvecolem2  24429  his35  24643  leopnmid  25695  oddpwdc  26882  subfacval2  27220  subfaclim  27221  circum  27464  clim2prod  27548  fallrisefac  27673  binomfallfaclem2  27688  faclimlem1  27694  faclimlem3  27696  faclim2  27699  bpolydiflem  28342  bpoly4  28347  itgmulc2nc  28609  dvcncxp1  28626  areacirclem1  28633  areacirclem4  28636  bfplem1  28870  pellexlem6  29324  rmxluc  29426  rmyluc2  29428  rmydbl  29430  jm2.18  29486  jm2.23  29494  jm2.27c  29505  jm3.1lem2  29516  proot1ex  29718  fmul01lt1lem1  29914  fmul01lt1lem2  29915  itgsinexplem1  29943  stoweidlem26  29970  wallispilem5  30013  wallispi  30014  wallispi2lem1  30015  wallispi2lem2  30016  stirlinglem3  30020  stirlinglem10  30027  stirlinglem15  30032  sigarls  30042  sharhght  30050  altgsumbcALT  30899