Theorem mulassd 8095

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

Syntax hints:   -> wi 4   = wceq 1372   e. wcel 2175  (class class class)co 5943   CCcc 7922   x. cmul 7929

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 8027

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

This theorem is referenced by:  ltmul1  8664  recexap  8725  mulap0  8726  mulcanapd  8733  receuap  8741  divmulasscomap  8768  divdivdivap  8785  divmuleqap  8789  conjmulap  8801  apmul1  8860  qapne  9759  modqmul1  10520  modqdi  10535  expadd  10724  mulbinom2  10799  binom3  10800  faclbnd  10884  faclbnd6  10887  bcm1k  10903  bcp1nk  10905  bcval5  10906  crre  11110  remullem  11124  resqrexlemcalc1  11267  resqrexlemnm  11271  amgm2  11371  binomlem  11736  geo2sum  11767  mertenslemi1  11788  clim2prod  11792  sinadd  11989  tanaddap  11992  dvdsmulcr  12074  dvdsmulgcd  12288  qredeq  12360  2sqpwodd  12440  pcaddlem  12604  prmpwdvds  12620  dvexp  15125  dvply1  15179  tangtx  15252  cxpmul  15326  binom4  15393  perfectlem1  15413  perfectlem2  15414  perfect  15415  lgsneg  15443  gausslemma2dlem6  15486  lgseisenlem1  15489  lgseisenlem2  15490  lgseisenlem3  15491  lgseisenlem4  15492  lgsquad2lem1  15500  lgsquad3  15503  2lgslem3a  15512  2lgslem3b  15513  2lgslem3c  15514  2lgslem3d  15515  2lgsoddprmlem2  15525  2sqlem3  15536