Theorem mulassd 8355

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 8316	. 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 6088   CCcc 8183   x. cmul 8190

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 8288

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

This theorem is used by:  ltmul1  8928  recexap  8989  mulap0  8990  mulcanapd  8997  receuap  9007  divmulasscomap  9034  divdivdivap  9051  divmuleqap  9055  conjmulap  9067  apmul1  9126  qapne  10054  modqmul1  10834  modqdi  10849  expadd  11038  mulbinom2  11113  binom3  11114  faclbnd  11200  faclbnd6  11203  bcm1k  11219  bcp1nk  11221  bcval5  11222  crre  11643  remullem  11657  sq01  11681  resqrexlemcalc1  11801  resqrexlemnm  11805  amgm2  11906  binomlem  12274  geo2sum  12305  mertenslemi1  12326  clim2prod  12330  sinadd  12527  tanaddap  12530  dvdsmulcr  12612  dvdsmulgcd  12826  qredeq  12898  2sqpwodd  12980  pcaddlem  13146  prmpwdvds  13162  dvexp  15954  dvply1  16008  tangtx  16082  logfac  16143  cxpmul  16162  binom4  16236  log2tlbndlog2  16237  chtqub  16313  perfectlem1  16316  perfectlem2  16317  perfect  16318  bcmono  16321  bclbnd  16324  bposlem9  16336  lgsneg  16365  gausslemma2dlem6  16408  lgseisenlem1  16411  lgseisenlem2  16412  lgseisenlem3  16413  lgseisenlem4  16414  lgsquad2lem1  16422  lgsquad3  16425  2lgslem3a  16434  2lgslem3b  16435  2lgslem3c  16436  2lgslem3d  16437  2lgsoddprmlem2  16447  2sqlem3  16458