Theorem mulassd 8202

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202  (class class class)co 6017   CCcc 8029   x. cmul 8036

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 8134

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

This theorem is referenced by:  ltmul1  8771  recexap  8832  mulap0  8833  mulcanapd  8840  receuap  8848  divmulasscomap  8875  divdivdivap  8892  divmuleqap  8896  conjmulap  8908  apmul1  8967  qapne  9872  modqmul1  10638  modqdi  10653  expadd  10842  mulbinom2  10917  binom3  10918  faclbnd  11002  faclbnd6  11005  bcm1k  11021  bcp1nk  11023  bcval5  11024  crre  11417  remullem  11431  resqrexlemcalc1  11574  resqrexlemnm  11578  amgm2  11678  binomlem  12043  geo2sum  12074  mertenslemi1  12095  clim2prod  12099  sinadd  12296  tanaddap  12299  dvdsmulcr  12381  dvdsmulgcd  12595  qredeq  12667  2sqpwodd  12747  pcaddlem  12911  prmpwdvds  12927  dvexp  15434  dvply1  15488  tangtx  15561  cxpmul  15635  binom4  15702  perfectlem1  15722  perfectlem2  15723  perfect  15724  lgsneg  15752  gausslemma2dlem6  15795  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgsquad2lem1  15809  lgsquad3  15812  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2lgsoddprmlem2  15834  2sqlem3  15845