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  8922  recexap  8983  mulap0  8984  mulcanapd  8991  receuap  9001  divmulasscomap  9028  divdivdivap  9045  divmuleqap  9049  conjmulap  9061  apmul1  9120  qapne  10048  modqmul1  10827  modqdi  10842  expadd  11031  mulbinom2  11106  binom3  11107  faclbnd  11193  faclbnd6  11196  bcm1k  11212  bcp1nk  11214  bcval5  11215  crre  11636  remullem  11650  sq01  11674  resqrexlemcalc1  11794  resqrexlemnm  11798  amgm2  11899  binomlem  12266  geo2sum  12297  mertenslemi1  12318  clim2prod  12322  sinadd  12519  tanaddap  12522  dvdsmulcr  12604  dvdsmulgcd  12818  qredeq  12890  2sqpwodd  12972  pcaddlem  13138  prmpwdvds  13154  dvexp  15861  dvply1  15915  tangtx  15989  logfac  16048  cxpmul  16067  binom4  16138  log2tlbndlog2  16139  perfectlem1  16197  perfectlem2  16198  perfect  16199  bcmono  16202  bclbnd  16205  lgsneg  16241  gausslemma2dlem6  16284  lgseisenlem1  16287  lgseisenlem2  16288  lgseisenlem3  16289  lgseisenlem4  16290  lgsquad2lem1  16298  lgsquad3  16301  2lgslem3a  16310  2lgslem3b  16311  2lgslem3c  16312  2lgslem3d  16313  2lgsoddprmlem2  16323  2sqlem3  16334