Theorem mulassd 9401

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

Syntax hints:   -> wi 4   = wceq 1369   e. wcel 1756  (class class class)co 6086   CCcc 9272   x. cmul 9279

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

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

This theorem is referenced by:  recex  9960  mulcand  9961  receu  9973  divdivdiv  10024  divmuleq  10028  conjmul  10040  modmul1  11744  moddi  11758  expadd  11898  binom3  11977  digit1  11990  discr1  11992  discr  11993  faclbnd  12058  faclbnd6  12067  bcm1k  12083  bcp1nk  12085  crre  12595  remullem  12609  amgm2  12849  iseraltlem2  13152  iseraltlem3  13153  binomlem  13284  climcndslem2  13305  geo2sum  13325  mertenslem1  13336  sinadd  13440  tanadd  13443  bezoutlem3  13716  dvdsmulgcd  13730  qredeq  13784  pcaddlem  13942  prmpwdvds  13957  ablfacrp  16555  nmoco  20291  cph2ass  20706  csbren  20873  minveclem2  20888  uniioombllem5  21042  itg1mulc  21157  mbfi1fseqlem5  21172  itgconst  21271  itgmulc2  21286  dvexp  21402  dvply1  21725  elqaalem3  21762  aalioulem1  21773  aaliou3lem2  21784  dvtaylp  21810  dvradcnv  21861  pserdvlem2  21868  tangtx  21942  tanregt0  21970  tanarg  22043  logcnlem4  22065  cxpmul  22108  dvcxp1  22155  root1eq1  22168  heron  22208  quad2  22209  dcubic1lem  22213  dcubic1  22215  cubic2  22218  binom4  22220  dquartlem1  22221  dquartlem2  22222  dquart  22223  quart1lem  22225  quart1  22226  quartlem1  22227  efiasin  22258  asinsinlem  22261  asinsin  22262  efiatan  22282  efiatan2  22287  2efiatan  22288  atantan  22293  atanbndlem  22295  atans2  22301  atantayl  22307  log2cnv  22314  log2tlbnd  22315  ftalem1  22385  ftalem5  22389  basellem3  22395  basellem5  22397  basellem8  22400  chtub  22526  perfectlem1  22543  perfectlem2  22544  perfect  22545  bcmono  22591  bclbnd  22594  bposlem9  22606  lgsneg  22633  lgseisenlem1  22663  lgseisenlem2  22664  lgseisenlem3  22665  lgseisenlem4  22666  lgsquad2lem1  22672  lgsquad3  22675  2sqlem3  22680  chto1ub  22700  rplogsumlem1  22708  dchrmusum2  22718  dchrvmasum2lem  22720  dchrvmasumlem2  22722  dchrvmasumiflem2  22726  dchrisum0lem1  22740  dchrisum0lem2  22742  mulog2sumlem2  22759  chpdifbndlem1  22777  selberg3lem1  22781  selberg4lem1  22784  selberg34r  22795  pntrlog2bndlem3  22803  pntrlog2bndlem5  22805  pntrlog2bndlem6  22807  pntlemh  22823  pntlemr  22826  pntlemf  22829  pntlemk  22830  pntlemo  22831  colinearalglem4  23106  axpasch  23138  axcontlem2  23162  axcontlem4  23164  axcontlem7  23167  axcontlem8  23168  ipasslem4  24185  minvecolem2  24227  his35  24441  leopnmid  25493  oddpwdc  26689  subfacval2  27027  subfaclim  27028  circum  27270  clim2prod  27354  fallrisefac  27479  binomfallfaclem2  27494  faclimlem1  27500  faclimlem3  27502  faclim2  27505  bpolydiflem  28148  bpoly4  28153  itgmulc2nc  28413  dvcncxp1  28430  areacirclem1  28437  areacirclem4  28440  bfplem1  28674  pellexlem6  29128  rmxluc  29230  rmyluc2  29232  rmydbl  29234  jm2.18  29290  jm2.23  29298  jm2.27c  29309  jm3.1lem2  29320  proot1ex  29522  fmul01lt1lem1  29718  fmul01lt1lem2  29719  itgsinexplem1  29747  stoweidlem26  29774  wallispilem5  29817  wallispi  29818  wallispi2lem1  29819  wallispi2lem2  29820  stirlinglem3  29824  stirlinglem10  29831  stirlinglem15  29836  sigarls  29846  sharhght  29854  altgsumbcALT  30701