Theorem mulassd 7661

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

Syntax hints:   -> wi 4   = wceq 1299   e. wcel 1448  (class class class)co 5706   CCcc 7498   x. cmul 7505

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

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

This theorem is referenced by:  ltmul1  8220  recexap  8275  mulap0  8276  mulcanapd  8283  receuap  8291  divmulasscomap  8317  divdivdivap  8334  divmuleqap  8338  conjmulap  8350  apmul1  8409  qapne  9281  modqmul1  9991  modqdi  10006  expadd  10176  mulbinom2  10249  binom3  10250  faclbnd  10328  faclbnd6  10331  bcm1k  10347  bcp1nk  10349  bcval5  10350  crre  10470  remullem  10484  resqrexlemcalc1  10626  resqrexlemnm  10630  amgm2  10730  binomlem  11091  geo2sum  11122  mertenslemi1  11143  sinadd  11241  tanaddap  11244  dvdsmulcr  11318  dvdsmulgcd  11506  qredeq  11570  2sqpwodd  11646