Theorem mulassd 8350

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8178   x. cmul 8185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-mulass 8283

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ltmul1  8923  recexap  8984  mulap0  8985  mulcanapd  8992  receuap  9002  divmulasscomap  9029  divdivdivap  9046  divmuleqap  9050  conjmulap  9062  apmul1  9121  qapne  10049  modqmul1  10829  modqdi  10844  expadd  11033  mulbinom2  11108  binom3  11109  faclbnd  11195  faclbnd6  11198  bcm1k  11214  bcp1nk  11216  bcval5  11217  crre  11638  remullem  11652  sq01  11676  resqrexlemcalc1  11796  resqrexlemnm  11800  amgm2  11901  binomlem  12269  geo2sum  12300  mertenslemi1  12321  clim2prod  12325  sinadd  12522  tanaddap  12525  dvdsmulcr  12607  dvdsmulgcd  12821  qredeq  12893  2sqpwodd  12975  pcaddlem  13141  prmpwdvds  13157  dvexp  15903  dvply1  15957  tangtx  16031  logfac  16090  cxpmul  16109  binom4  16180  log2tlbndlog2  16181  chtqub  16257  perfectlem1  16260  perfectlem2  16261  perfect  16262  bcmono  16265  bclbnd  16268  bposlem9  16280  lgsneg  16309  gausslemma2dlem6  16352  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgseisenlem4  16358  lgsquad2lem1  16366  lgsquad3  16369  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2lgsoddprmlem2  16391  2sqlem3  16402