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  10055  modqmul1  10835  modqdi  10850  expadd  11039  mulbinom2  11114  binom3  11115  faclbnd  11201  faclbnd6  11204  bcm1k  11220  bcp1nk  11222  bcval5  11223  crre  11644  remullem  11658  sq01  11682  resqrexlemcalc1  11802  resqrexlemnm  11806  amgm2  11907  binomlem  12275  geo2sum  12306  mertenslemi1  12327  clim2prod  12331  sinadd  12528  tanaddap  12531  dvdsmulcr  12613  dvdsmulgcd  12827  qredeq  12899  2sqpwodd  12981  pcaddlem  13147  prmpwdvds  13163  dvexp  15937  dvply1  15991  tangtx  16065  logfac  16126  cxpmul  16145  binom4  16219  log2tlbndlog2  16220  chtqub  16296  perfectlem1  16299  perfectlem2  16300  perfect  16301  bcmono  16304  bclbnd  16307  bposlem9  16319  lgsneg  16348  gausslemma2dlem6  16391  lgseisenlem1  16394  lgseisenlem2  16395  lgseisenlem3  16396  lgseisenlem4  16397  lgsquad2lem1  16405  lgsquad3  16408  2lgslem3a  16417  2lgslem3b  16418  2lgslem3c  16419  2lgslem3d  16420  2lgsoddprmlem2  16430  2sqlem3  16441