Theorem mulassd 8349

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402   e. wcel 2209  (class class class)co 6085   CCcc 8177   x. cmul 8184

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-mulass 8282

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  ltmul1  8920  recexap  8981  mulap0  8982  mulcanapd  8989  receuap  8999  divmulasscomap  9026  divdivdivap  9043  divmuleqap  9047  conjmulap  9059  apmul1  9118  qapne  10039  modqmul1  10814  modqdi  10829  expadd  11018  mulbinom2  11093  binom3  11094  faclbnd  11179  faclbnd6  11182  bcm1k  11198  bcp1nk  11200  bcval5  11201  crre  11622  remullem  11636  sq01  11660  resqrexlemcalc1  11780  resqrexlemnm  11784  amgm2  11884  binomlem  12250  geo2sum  12281  mertenslemi1  12302  clim2prod  12306  sinadd  12503  tanaddap  12506  dvdsmulcr  12588  dvdsmulgcd  12802  qredeq  12874  2sqpwodd  12954  pcaddlem  13118  prmpwdvds  13134  dvexp  15812  dvply1  15866  tangtx  15939  logfac  15995  cxpmul  16014  binom4  16081  log2tlbndlog2  16082  perfectlem1  16113  perfectlem2  16114  perfect  16115  lgsneg  16143  gausslemma2dlem6  16186  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisenlem4  16192  lgsquad2lem1  16200  lgsquad3  16203  2lgslem3a  16212  2lgslem3b  16213  2lgslem3c  16214  2lgslem3d  16215  2lgsoddprmlem2  16225  2sqlem3  16236