Theorem mulassd 8313

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

Syntax hints:   -> wi 4   = wceq 1398   e. wcel 2205  (class class class)co 6058   CCcc 8141   x. cmul 8148

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 8246

This theorem depends on definitions:  df-bi 117  df-3an 1007

This theorem is referenced by:  ltmul1  8883  recexap  8944  mulap0  8945  mulcanapd  8952  receuap  8960  divmulasscomap  8987  divdivdivap  9004  divmuleqap  9008  conjmulap  9020  apmul1  9079  qapne  9989  modqmul1  10763  modqdi  10778  expadd  10967  mulbinom2  11042  binom3  11043  faclbnd  11128  faclbnd6  11131  bcm1k  11147  bcp1nk  11149  bcval5  11150  crre  11567  remullem  11581  resqrexlemcalc1  11724  resqrexlemnm  11728  amgm2  11828  binomlem  12194  geo2sum  12225  mertenslemi1  12246  clim2prod  12250  sinadd  12447  tanaddap  12450  dvdsmulcr  12532  dvdsmulgcd  12746  qredeq  12818  2sqpwodd  12898  pcaddlem  13062  prmpwdvds  13078  dvexp  15702  dvply1  15756  tangtx  15829  cxpmul  15903  binom4  15970  perfectlem1  15993  perfectlem2  15994  perfect  15995  lgsneg  16023  gausslemma2dlem6  16066  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  lgsquad2lem1  16080  lgsquad3  16083  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2lgsoddprmlem2  16105  2sqlem3  16116