Theorem mulassd 8297

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 8258	. 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 2203  (class class class)co 6050   CCcc 8125   x. cmul 8132

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 8230

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

This theorem is referenced by:  ltmul1  8866  recexap  8927  mulap0  8928  mulcanapd  8935  receuap  8943  divmulasscomap  8970  divdivdivap  8987  divmuleqap  8991  conjmulap  9003  apmul1  9062  qapne  9971  modqmul1  10739  modqdi  10754  expadd  10943  mulbinom2  11018  binom3  11019  faclbnd  11103  faclbnd6  11106  bcm1k  11122  bcp1nk  11124  bcval5  11125  crre  11542  remullem  11556  resqrexlemcalc1  11699  resqrexlemnm  11703  amgm2  11803  binomlem  12169  geo2sum  12200  mertenslemi1  12221  clim2prod  12225  sinadd  12422  tanaddap  12425  dvdsmulcr  12507  dvdsmulgcd  12721  qredeq  12793  2sqpwodd  12873  pcaddlem  13037  prmpwdvds  13053  dvexp  15576  dvply1  15630  tangtx  15703  cxpmul  15777  binom4  15844  perfectlem1  15867  perfectlem2  15868  perfect  15869  lgsneg  15897  gausslemma2dlem6  15940  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgsquad2lem1  15954  lgsquad3  15957  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2lgsoddprmlem2  15979  2sqlem3  15990