Theorem mulassd 9397

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

Syntax hints:   -> wi 4   = wceq 1362   e. wcel 1755  (class class class)co 6080   CCcc 9268   x. cmul 9275

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

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

This theorem is referenced by:  recex  9956  mulcand  9957  receu  9969  divdivdiv  10020  divmuleq  10024  conjmul  10036  modmul1  11736  moddi  11750  expadd  11890  binom3  11969  digit1  11982  discr1  11984  discr  11985  faclbnd  12050  faclbnd6  12059  bcm1k  12075  bcp1nk  12077  crre  12587  remullem  12601  amgm2  12841  iseraltlem2  13144  iseraltlem3  13145  binomlem  13275  climcndslem2  13296  geo2sum  13316  mertenslem1  13327  sinadd  13431  tanadd  13434  bezoutlem3  13707  dvdsmulgcd  13721  qredeq  13775  pcaddlem  13933  prmpwdvds  13948  ablfacrp  16541  nmoco  20158  cph2ass  20573  csbren  20740  minveclem2  20755  uniioombllem5  20909  itg1mulc  21024  mbfi1fseqlem5  21039  itgconst  21138  itgmulc2  21153  dvexp  21269  dvply1  21635  elqaalem3  21672  aalioulem1  21683  aaliou3lem2  21694  dvtaylp  21720  dvradcnv  21771  pserdvlem2  21778  tangtx  21852  tanregt0  21880  tanarg  21953  logcnlem4  21975  cxpmul  22018  dvcxp1  22065  root1eq1  22078  heron  22118  quad2  22119  dcubic1lem  22123  dcubic1  22125  cubic2  22128  binom4  22130  dquartlem1  22131  dquartlem2  22132  dquart  22133  quart1lem  22135  quart1  22136  quartlem1  22137  efiasin  22168  asinsinlem  22171  asinsin  22172  efiatan  22192  efiatan2  22197  2efiatan  22198  atantan  22203  atanbndlem  22205  atans2  22211  atantayl  22217  log2cnv  22224  log2tlbnd  22225  ftalem1  22295  ftalem5  22299  basellem3  22305  basellem5  22307  basellem8  22310  chtub  22436  perfectlem1  22453  perfectlem2  22454  perfect  22455  bcmono  22501  bclbnd  22504  bposlem9  22516  lgsneg  22543  lgseisenlem1  22573  lgseisenlem2  22574  lgseisenlem3  22575  lgseisenlem4  22576  lgsquad2lem1  22582  lgsquad3  22585  2sqlem3  22590  chto1ub  22610  rplogsumlem1  22618  dchrmusum2  22628  dchrvmasum2lem  22630  dchrvmasumlem2  22632  dchrvmasumiflem2  22636  dchrisum0lem1  22650  dchrisum0lem2  22652  mulog2sumlem2  22669  chpdifbndlem1  22687  selberg3lem1  22691  selberg4lem1  22694  selberg34r  22705  pntrlog2bndlem3  22713  pntrlog2bndlem5  22715  pntrlog2bndlem6  22717  pntlemh  22733  pntlemr  22736  pntlemf  22739  pntlemk  22740  pntlemo  22741  colinearalglem4  22978  axpasch  23010  axcontlem2  23034  axcontlem4  23036  axcontlem7  23039  axcontlem8  23040  ipasslem4  24057  minvecolem2  24099  his35  24313  leopnmid  25365  oddpwdc  26585  subfacval2  26923  subfaclim  26924  circum  27166  clim2prod  27250  fallrisefac  27375  binomfallfaclem2  27390  faclimlem1  27396  faclimlem3  27398  faclim2  27401  bpolydiflem  28044  bpoly4  28049  itgmulc2nc  28304  dvcncxp1  28321  areacirclem1  28328  areacirclem4  28331  bfplem1  28565  pellexlem6  29020  rmxluc  29122  rmyluc2  29124  rmydbl  29126  jm2.18  29182  jm2.23  29190  jm2.27c  29201  jm3.1lem2  29212  proot1ex  29414  fmul01lt1lem1  29610  fmul01lt1lem2  29611  itgsinexplem1  29640  stoweidlem26  29667  wallispilem5  29710  wallispi  29711  wallispi2lem1  29712  wallispi2lem2  29713  stirlinglem3  29717  stirlinglem10  29724  stirlinglem15  29729  sigarls  29739  sharhght  29747