Theorem mulassd 8166

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200  (class class class)co 6000   CCcc 7993   x. cmul 8000

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 8098

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

This theorem is referenced by:  ltmul1  8735  recexap  8796  mulap0  8797  mulcanapd  8804  receuap  8812  divmulasscomap  8839  divdivdivap  8856  divmuleqap  8860  conjmulap  8872  apmul1  8931  qapne  9830  modqmul1  10594  modqdi  10609  expadd  10798  mulbinom2  10873  binom3  10874  faclbnd  10958  faclbnd6  10961  bcm1k  10977  bcp1nk  10979  bcval5  10980  crre  11363  remullem  11377  resqrexlemcalc1  11520  resqrexlemnm  11524  amgm2  11624  binomlem  11989  geo2sum  12020  mertenslemi1  12041  clim2prod  12045  sinadd  12242  tanaddap  12245  dvdsmulcr  12327  dvdsmulgcd  12541  qredeq  12613  2sqpwodd  12693  pcaddlem  12857  prmpwdvds  12873  dvexp  15379  dvply1  15433  tangtx  15506  cxpmul  15580  binom4  15647  perfectlem1  15667  perfectlem2  15668  perfect  15669  lgsneg  15697  gausslemma2dlem6  15740  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  lgsquad2lem1  15754  lgsquad3  15757  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2lgsoddprmlem2  15779  2sqlem3  15790