Theorem mulassd 7913

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

Syntax hints:   -> wi 4   = wceq 1342   e. wcel 2135  (class class class)co 5836   CCcc 7742   x. cmul 7749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-mulass 7847

This theorem depends on definitions:  df-bi 116  df-3an 969

This theorem is referenced by:  ltmul1  8481  recexap  8541  mulap0  8542  mulcanapd  8549  receuap  8557  divmulasscomap  8583  divdivdivap  8600  divmuleqap  8604  conjmulap  8616  apmul1  8675  qapne  9568  modqmul1  10302  modqdi  10317  expadd  10487  mulbinom2  10560  binom3  10561  faclbnd  10643  faclbnd6  10646  bcm1k  10662  bcp1nk  10664  bcval5  10665  crre  10785  remullem  10799  resqrexlemcalc1  10942  resqrexlemnm  10946  amgm2  11046  binomlem  11410  geo2sum  11441  mertenslemi1  11462  clim2prod  11466  sinadd  11663  tanaddap  11666  dvdsmulcr  11747  dvdsmulgcd  11943  qredeq  12007  2sqpwodd  12085  pcaddlem  12247  dvexp  13216  tangtx  13300  cxpmul  13374  binom4  13438