Theorem mulassd 7782

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

Syntax hints:   -> wi 4   = wceq 1331   e. wcel 1480  (class class class)co 5767   CCcc 7611   x. cmul 7618

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  ltmul1  8347  recexap  8407  mulap0  8408  mulcanapd  8415  receuap  8423  divmulasscomap  8449  divdivdivap  8466  divmuleqap  8470  conjmulap  8482  apmul1  8541  qapne  9424  modqmul1  10143  modqdi  10158  expadd  10328  mulbinom2  10401  binom3  10402  faclbnd  10480  faclbnd6  10483  bcm1k  10499  bcp1nk  10501  bcval5  10502  crre  10622  remullem  10636  resqrexlemcalc1  10779  resqrexlemnm  10783  amgm2  10883  binomlem  11245  geo2sum  11276  mertenslemi1  11297  clim2prod  11301  sinadd  11432  tanaddap  11435  dvdsmulcr  11512  dvdsmulgcd  11702  qredeq  11766  2sqpwodd  11843  dvexp  12833  tangtx  12908