Theorem mulassd 8006

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2160  (class class class)co 5892   CCcc 7834   x. cmul 7841

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 7939

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

This theorem is referenced by:  ltmul1  8574  recexap  8635  mulap0  8636  mulcanapd  8643  receuap  8651  divmulasscomap  8678  divdivdivap  8695  divmuleqap  8699  conjmulap  8711  apmul1  8770  qapne  9664  modqmul1  10403  modqdi  10418  expadd  10588  mulbinom2  10663  binom3  10664  faclbnd  10748  faclbnd6  10751  bcm1k  10767  bcp1nk  10769  bcval5  10770  crre  10893  remullem  10907  resqrexlemcalc1  11050  resqrexlemnm  11054  amgm2  11154  binomlem  11518  geo2sum  11549  mertenslemi1  11570  clim2prod  11574  sinadd  11771  tanaddap  11774  dvdsmulcr  11855  dvdsmulgcd  12053  qredeq  12123  2sqpwodd  12203  pcaddlem  12366  prmpwdvds  12382  dvexp  14612  tangtx  14696  cxpmul  14770  binom4  14834  lgsneg  14863  lgseisenlem1  14888  lgseisenlem2  14889  2lgsoddprmlem2  14892  2sqlem3  14902