Theorem mulassd 8245

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2202  (class class class)co 6028   CCcc 8073   x. cmul 8080

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 8178

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

This theorem is referenced by:  ltmul1  8814  recexap  8875  mulap0  8876  mulcanapd  8883  receuap  8891  divmulasscomap  8918  divdivdivap  8935  divmuleqap  8939  conjmulap  8951  apmul1  9010  qapne  9917  modqmul1  10685  modqdi  10700  expadd  10889  mulbinom2  10964  binom3  10965  faclbnd  11049  faclbnd6  11052  bcm1k  11068  bcp1nk  11070  bcval5  11071  crre  11480  remullem  11494  resqrexlemcalc1  11637  resqrexlemnm  11641  amgm2  11741  binomlem  12107  geo2sum  12138  mertenslemi1  12159  clim2prod  12163  sinadd  12360  tanaddap  12363  dvdsmulcr  12445  dvdsmulgcd  12659  qredeq  12731  2sqpwodd  12811  pcaddlem  12975  prmpwdvds  12991  dvexp  15505  dvply1  15559  tangtx  15632  cxpmul  15706  binom4  15773  perfectlem1  15796  perfectlem2  15797  perfect  15798  lgsneg  15826  gausslemma2dlem6  15869  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgsquad2lem1  15883  lgsquad3  15886  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  2lgsoddprmlem2  15908  2sqlem3  15919