Theorem mulassd 7943

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

Syntax hints:   -> wi 4   = wceq 1348   e. wcel 2141  (class class class)co 5853   CCcc 7772   x. cmul 7779

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 7877

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

This theorem is referenced by:  ltmul1  8511  recexap  8571  mulap0  8572  mulcanapd  8579  receuap  8587  divmulasscomap  8613  divdivdivap  8630  divmuleqap  8634  conjmulap  8646  apmul1  8705  qapne  9598  modqmul1  10333  modqdi  10348  expadd  10518  mulbinom2  10592  binom3  10593  faclbnd  10675  faclbnd6  10678  bcm1k  10694  bcp1nk  10696  bcval5  10697  crre  10821  remullem  10835  resqrexlemcalc1  10978  resqrexlemnm  10982  amgm2  11082  binomlem  11446  geo2sum  11477  mertenslemi1  11498  clim2prod  11502  sinadd  11699  tanaddap  11702  dvdsmulcr  11783  dvdsmulgcd  11980  qredeq  12050  2sqpwodd  12130  pcaddlem  12292  prmpwdvds  12307  dvexp  13469  tangtx  13553  cxpmul  13627  binom4  13691  lgsneg  13719  2sqlem3  13747