Theorem mulassd 8339

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 8300	. 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 ) ) )

Syntax hints:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6075   CCcc 8167   x. cmul 8174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-mulass 8272

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

This theorem is referenced by:  ltmul1  8910  recexap  8971  mulap0  8972  mulcanapd  8979  receuap  8989  divmulasscomap  9016  divdivdivap  9033  divmuleqap  9037  conjmulap  9049  apmul1  9108  qapne  10018  modqmul1  10792  modqdi  10807  expadd  10996  mulbinom2  11071  binom3  11072  faclbnd  11157  faclbnd6  11160  bcm1k  11176  bcp1nk  11178  bcval5  11179  crre  11600  remullem  11614  sq01  11638  resqrexlemcalc1  11758  resqrexlemnm  11762  amgm2  11862  binomlem  12228  geo2sum  12259  mertenslemi1  12280  clim2prod  12284  sinadd  12481  tanaddap  12484  dvdsmulcr  12566  dvdsmulgcd  12780  qredeq  12852  2sqpwodd  12932  pcaddlem  13096  prmpwdvds  13112  dvexp  15735  dvply1  15789  tangtx  15862  logfac  15918  cxpmul  15937  binom4  16004  perfectlem1  16027  perfectlem2  16028  perfect  16029  lgsneg  16057  gausslemma2dlem6  16100  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgsquad2lem1  16114  lgsquad3  16117  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2lgsoddprmlem2  16139  2sqlem3  16150