Theorem mulassd 9615

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

Syntax hints:   -> wi 4   = wceq 1379   e. wcel 1767  (class class class)co 6282   CCcc 9486   x. cmul 9493

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

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

This theorem is referenced by:  recex  10177  mulcand  10178  receu  10190  divdivdiv  10241  divmuleq  10245  conjmul  10257  modmul1  12003  moddi  12017  expadd  12170  binom3  12249  digit1  12262  discr1  12264  discr  12265  faclbnd  12330  faclbnd6  12339  bcm1k  12355  bcp1nk  12357  crre  12904  remullem  12918  amgm2  13158  iseraltlem2  13461  iseraltlem3  13462  binomlem  13597  climcndslem2  13618  geo2sum  13638  mertenslem1  13649  sinadd  13753  tanadd  13756  bezoutlem3  14030  dvdsmulgcd  14044  qredeq  14099  pcaddlem  14259  prmpwdvds  14274  ablfacrp  16904  nmoco  20976  cph2ass  21391  csbren  21558  minveclem2  21573  uniioombllem5  21728  itg1mulc  21843  mbfi1fseqlem5  21858  itgconst  21957  itgmulc2  21972  dvexp  22088  dvply1  22411  elqaalem3  22448  aalioulem1  22459  aaliou3lem2  22470  dvtaylp  22496  dvradcnv  22547  pserdvlem2  22554  tangtx  22628  tanregt0  22656  tanarg  22729  logcnlem4  22751  cxpmul  22794  dvcxp1  22841  root1eq1  22854  heron  22894  quad2  22895  dcubic1lem  22899  dcubic1  22901  cubic2  22904  binom4  22906  dquartlem1  22907  dquartlem2  22908  dquart  22909  quart1lem  22911  quart1  22912  quartlem1  22913  efiasin  22944  asinsinlem  22947  asinsin  22948  efiatan  22968  efiatan2  22973  2efiatan  22974  atantan  22979  atanbndlem  22981  atans2  22987  atantayl  22993  log2cnv  23000  log2tlbnd  23001  ftalem1  23071  ftalem5  23075  basellem3  23081  basellem5  23083  basellem8  23086  chtub  23212  perfectlem1  23229  perfectlem2  23230  perfect  23231  bcmono  23277  bclbnd  23280  bposlem9  23292  lgsneg  23319  lgseisenlem1  23349  lgseisenlem2  23350  lgseisenlem3  23351  lgseisenlem4  23352  lgsquad2lem1  23358  lgsquad3  23361  2sqlem3  23366  chto1ub  23386  rplogsumlem1  23394  dchrmusum2  23404  dchrvmasum2lem  23406  dchrvmasumlem2  23408  dchrvmasumiflem2  23412  dchrisum0lem1  23426  dchrisum0lem2  23428  mulog2sumlem2  23445  chpdifbndlem1  23463  selberg3lem1  23467  selberg4lem1  23470  selberg34r  23481  pntrlog2bndlem3  23489  pntrlog2bndlem5  23491  pntrlog2bndlem6  23493  pntlemh  23509  pntlemr  23512  pntlemf  23515  pntlemk  23516  pntlemo  23517  colinearalglem4  23885  axpasch  23917  axcontlem2  23941  axcontlem4  23943  axcontlem7  23946  axcontlem8  23947  ipasslem4  25422  minvecolem2  25464  his35  25678  leopnmid  26730  oddpwdc  27930  subfacval2  28268  subfaclim  28269  circum  28512  clim2prod  28596  fallrisefac  28721  binomfallfaclem2  28736  faclimlem1  28742  faclimlem3  28744  faclim2  28747  bpolydiflem  29390  bpoly4  29395  itgmulc2nc  29658  dvcncxp1  29675  areacirclem1  29682  areacirclem4  29685  bfplem1  29919  pellexlem6  30372  rmxluc  30474  rmyluc2  30476  rmydbl  30478  jm2.18  30534  jm2.23  30542  jm2.27c  30553  jm3.1lem2  30564  proot1ex  30766  mul13d  31038  fmul01lt1lem1  31134  fmul01lt1lem2  31135  coskpi2  31202  cosknegpi  31205  itgsinexplem1  31271  stoweidlem26  31326  wallispilem5  31369  wallispi  31370  wallispi2lem1  31371  wallispi2lem2  31372  stirlinglem3  31376  stirlinglem10  31383  stirlinglem15  31388  dirkertrigeqlem1  31398  dirkertrigeqlem2  31399  dirkertrigeqlem3  31400  dirkertrigeq  31401  dirkercncflem2  31404  fourierdlem66  31473  fourierswlem  31531  fouriersw  31532  sigarls  31541  sharhght  31549  altgsumbcALT  32006