Theorem mulassd 8203

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202  (class class class)co 6018   CCcc 8030   x. cmul 8037

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 8135

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

This theorem is referenced by:  ltmul1  8772  recexap  8833  mulap0  8834  mulcanapd  8841  receuap  8849  divmulasscomap  8876  divdivdivap  8893  divmuleqap  8897  conjmulap  8909  apmul1  8968  qapne  9873  modqmul1  10640  modqdi  10655  expadd  10844  mulbinom2  10919  binom3  10920  faclbnd  11004  faclbnd6  11007  bcm1k  11023  bcp1nk  11025  bcval5  11026  crre  11435  remullem  11449  resqrexlemcalc1  11592  resqrexlemnm  11596  amgm2  11696  binomlem  12062  geo2sum  12093  mertenslemi1  12114  clim2prod  12118  sinadd  12315  tanaddap  12318  dvdsmulcr  12400  dvdsmulgcd  12614  qredeq  12686  2sqpwodd  12766  pcaddlem  12930  prmpwdvds  12946  dvexp  15454  dvply1  15508  tangtx  15581  cxpmul  15655  binom4  15722  perfectlem1  15742  perfectlem2  15743  perfect  15744  lgsneg  15772  gausslemma2dlem6  15815  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgsquad2lem1  15829  lgsquad3  15832  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2lgsoddprmlem2  15854  2sqlem3  15865