Theorem mulassd 8181

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 8141	. 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 6007   CCcc 8008   x. cmul 8015

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 8113

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

This theorem is referenced by:  ltmul1  8750  recexap  8811  mulap0  8812  mulcanapd  8819  receuap  8827  divmulasscomap  8854  divdivdivap  8871  divmuleqap  8875  conjmulap  8887  apmul1  8946  qapne  9846  modqmul1  10611  modqdi  10626  expadd  10815  mulbinom2  10890  binom3  10891  faclbnd  10975  faclbnd6  10978  bcm1k  10994  bcp1nk  10996  bcval5  10997  crre  11383  remullem  11397  resqrexlemcalc1  11540  resqrexlemnm  11544  amgm2  11644  binomlem  12009  geo2sum  12040  mertenslemi1  12061  clim2prod  12065  sinadd  12262  tanaddap  12265  dvdsmulcr  12347  dvdsmulgcd  12561  qredeq  12633  2sqpwodd  12713  pcaddlem  12877  prmpwdvds  12893  dvexp  15400  dvply1  15454  tangtx  15527  cxpmul  15601  binom4  15668  perfectlem1  15688  perfectlem2  15689  perfect  15690  lgsneg  15718  gausslemma2dlem6  15761  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgseisenlem4  15767  lgsquad2lem1  15775  lgsquad3  15778  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2lgsoddprmlem2  15800  2sqlem3  15811