Theorem mulassd 7193

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

Syntax hints:   -> wi 4   = wceq 1285   e. wcel 1434  (class class class)co 5537   CCcc 7030   x. cmul 7037

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

This theorem depends on definitions:  df-bi 115  df-3an 922

This theorem is referenced by:  ltmul1  7748  recexap  7799  mulap0  7800  mulcanapd  7807  receuap  7815  divmulasscomap  7840  divdivdivap  7857  divmuleqap  7861  conjmulap  7873  apmul1  7932  qapne  8794  modqmul1  9448  modqdi  9463  expadd  9604  mulbinom2  9675  binom3  9676  faclbnd  9754  faclbnd6  9757  bcm1k  9773  bcp1nk  9775  ibcval5  9776  crre  9871  remullem  9885  resqrexlemcalc1  10027  resqrexlemnm  10031  amgm2  10131  dvdsmulcr  10359  dvdsmulgcd  10547  qredeq  10611  2sqpwodd  10687