Theorem mulassd 7789

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

Syntax hints:   -> wi 4   = wceq 1331   e. wcel 1480  (class class class)co 5774   CCcc 7618   x. cmul 7625

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 7723

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

This theorem is referenced by:  ltmul1  8354  recexap  8414  mulap0  8415  mulcanapd  8422  receuap  8430  divmulasscomap  8456  divdivdivap  8473  divmuleqap  8477  conjmulap  8489  apmul1  8548  qapne  9431  modqmul1  10150  modqdi  10165  expadd  10335  mulbinom2  10408  binom3  10409  faclbnd  10487  faclbnd6  10490  bcm1k  10506  bcp1nk  10508  bcval5  10509  crre  10629  remullem  10643  resqrexlemcalc1  10786  resqrexlemnm  10790  amgm2  10890  binomlem  11252  geo2sum  11283  mertenslemi1  11304  clim2prod  11308  sinadd  11443  tanaddap  11446  dvdsmulcr  11523  dvdsmulgcd  11713  qredeq  11777  2sqpwodd  11854  dvexp  12844  tangtx  12919