Theorem mulassd 7142

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

Syntax hints:   -> wi 4   = wceq 1284   e. wcel 1433  (class class class)co 5532   CCcc 6979   x. cmul 6986

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 7079

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

This theorem is referenced by:  ltmul1  7692  recexap  7743  mulap0  7744  mulcanapd  7751  receuap  7759  divmulasscomap  7784  divdivdivap  7801  divmuleqap  7805  conjmulap  7817  apmul1  7876  qapne  8724  modqmul1  9379  modqdi  9394  expadd  9518  mulbinom2  9589  binom3  9590  faclbnd  9668  faclbnd6  9671  bcm1k  9687  bcp1nk  9689  ibcval5  9690  crre  9744  remullem  9758  resqrexlemcalc1  9900  resqrexlemnm  9904  amgm2  10004  dvdsmulcr  10225  dvdsmulgcd  10414  qredeq  10478  2sqpwodd  10554