Theorem mulassd 8126

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2177  (class class class)co 5962   CCcc 7953   x. cmul 7960

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 8058

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

This theorem is referenced by:  ltmul1  8695  recexap  8756  mulap0  8757  mulcanapd  8764  receuap  8772  divmulasscomap  8799  divdivdivap  8816  divmuleqap  8820  conjmulap  8832  apmul1  8891  qapne  9790  modqmul1  10554  modqdi  10569  expadd  10758  mulbinom2  10833  binom3  10834  faclbnd  10918  faclbnd6  10921  bcm1k  10937  bcp1nk  10939  bcval5  10940  crre  11253  remullem  11267  resqrexlemcalc1  11410  resqrexlemnm  11414  amgm2  11514  binomlem  11879  geo2sum  11910  mertenslemi1  11931  clim2prod  11935  sinadd  12132  tanaddap  12135  dvdsmulcr  12217  dvdsmulgcd  12431  qredeq  12503  2sqpwodd  12583  pcaddlem  12747  prmpwdvds  12763  dvexp  15268  dvply1  15322  tangtx  15395  cxpmul  15469  binom4  15536  perfectlem1  15556  perfectlem2  15557  perfect  15558  lgsneg  15586  gausslemma2dlem6  15629  lgseisenlem1  15632  lgseisenlem2  15633  lgseisenlem3  15634  lgseisenlem4  15635  lgsquad2lem1  15643  lgsquad3  15646  2lgslem3a  15655  2lgslem3b  15656  2lgslem3c  15657  2lgslem3d  15658  2lgsoddprmlem2  15668  2sqlem3  15679