Theorem mulassd 7975

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

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148  (class class class)co 5870   CCcc 7804   x. cmul 7811

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 7909

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

This theorem is referenced by:  ltmul1  8543  recexap  8604  mulap0  8605  mulcanapd  8612  receuap  8620  divmulasscomap  8647  divdivdivap  8664  divmuleqap  8668  conjmulap  8680  apmul1  8739  qapne  9633  modqmul1  10370  modqdi  10385  expadd  10555  mulbinom2  10629  binom3  10630  faclbnd  10712  faclbnd6  10715  bcm1k  10731  bcp1nk  10733  bcval5  10734  crre  10857  remullem  10871  resqrexlemcalc1  11014  resqrexlemnm  11018  amgm2  11118  binomlem  11482  geo2sum  11513  mertenslemi1  11534  clim2prod  11538  sinadd  11735  tanaddap  11738  dvdsmulcr  11819  dvdsmulgcd  12016  qredeq  12086  2sqpwodd  12166  pcaddlem  12328  prmpwdvds  12343  dvexp  13957  tangtx  14041  cxpmul  14115  binom4  14179  lgsneg  14207  2sqlem3  14235