Theorem mulassd 7922

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

Syntax hints:   -> wi 4   = wceq 1343   e. wcel 2136  (class class class)co 5842   CCcc 7751   x. cmul 7758

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 7856

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

This theorem is referenced by:  ltmul1  8490  recexap  8550  mulap0  8551  mulcanapd  8558  receuap  8566  divmulasscomap  8592  divdivdivap  8609  divmuleqap  8613  conjmulap  8625  apmul1  8684  qapne  9577  modqmul1  10312  modqdi  10327  expadd  10497  mulbinom2  10571  binom3  10572  faclbnd  10654  faclbnd6  10657  bcm1k  10673  bcp1nk  10675  bcval5  10676  crre  10799  remullem  10813  resqrexlemcalc1  10956  resqrexlemnm  10960  amgm2  11060  binomlem  11424  geo2sum  11455  mertenslemi1  11476  clim2prod  11480  sinadd  11677  tanaddap  11680  dvdsmulcr  11761  dvdsmulgcd  11958  qredeq  12028  2sqpwodd  12108  pcaddlem  12270  prmpwdvds  12285  dvexp  13325  tangtx  13409  cxpmul  13483  binom4  13547  lgsneg  13575  2sqlem3  13603