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  11139  remullem  11153  resqrexlemcalc1  11296  resqrexlemnm  11300  amgm2  11400  binomlem  11765  geo2sum  11796  mertenslemi1  11817  clim2prod  11821  sinadd  12018  tanaddap  12021  dvdsmulcr  12103  dvdsmulgcd  12317  qredeq  12389  2sqpwodd  12469  pcaddlem  12633  prmpwdvds  12649  dvexp  15154  dvply1  15208  tangtx  15281  cxpmul  15355  binom4  15422  perfectlem1  15442  perfectlem2  15443  perfect  15444  lgsneg  15472  gausslemma2dlem6  15515  lgseisenlem1  15518  lgseisenlem2  15519  lgseisenlem3  15520  lgseisenlem4  15521  lgsquad2lem1  15529  lgsquad3  15532  2lgslem3a  15541  2lgslem3b  15542  2lgslem3c  15543  2lgslem3d  15544  2lgsoddprmlem2  15554  2sqlem3  15565