Theorem mulassd 7936

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

Syntax hints:   -> wi 4   = wceq 1348   e. wcel 2141  (class class class)co 5851   CCcc 7765   x. cmul 7772

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 7870

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

This theorem is referenced by:  ltmul1  8504  recexap  8564  mulap0  8565  mulcanapd  8572  receuap  8580  divmulasscomap  8606  divdivdivap  8623  divmuleqap  8627  conjmulap  8639  apmul1  8698  qapne  9591  modqmul1  10326  modqdi  10341  expadd  10511  mulbinom2  10585  binom3  10586  faclbnd  10668  faclbnd6  10671  bcm1k  10687  bcp1nk  10689  bcval5  10690  crre  10814  remullem  10828  resqrexlemcalc1  10971  resqrexlemnm  10975  amgm2  11075  binomlem  11439  geo2sum  11470  mertenslemi1  11491  clim2prod  11495  sinadd  11692  tanaddap  11695  dvdsmulcr  11776  dvdsmulgcd  11973  qredeq  12043  2sqpwodd  12123  pcaddlem  12285  prmpwdvds  12300  dvexp  13434  tangtx  13518  cxpmul  13592  binom4  13656  lgsneg  13684  2sqlem3  13712