Theorem mulassd 8193

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200  (class class class)co 6013   CCcc 8020   x. cmul 8027

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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  ltmul1  8762  recexap  8823  mulap0  8824  mulcanapd  8831  receuap  8839  divmulasscomap  8866  divdivdivap  8883  divmuleqap  8887  conjmulap  8899  apmul1  8958  qapne  9863  modqmul1  10629  modqdi  10644  expadd  10833  mulbinom2  10908  binom3  10909  faclbnd  10993  faclbnd6  10996  bcm1k  11012  bcp1nk  11014  bcval5  11015  crre  11408  remullem  11422  resqrexlemcalc1  11565  resqrexlemnm  11569  amgm2  11669  binomlem  12034  geo2sum  12065  mertenslemi1  12086  clim2prod  12090  sinadd  12287  tanaddap  12290  dvdsmulcr  12372  dvdsmulgcd  12586  qredeq  12658  2sqpwodd  12738  pcaddlem  12902  prmpwdvds  12918  dvexp  15425  dvply1  15479  tangtx  15552  cxpmul  15626  binom4  15693  perfectlem1  15713  perfectlem2  15714  perfect  15715  lgsneg  15743  gausslemma2dlem6  15786  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgsquad2lem1  15800  lgsquad3  15803  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2lgsoddprmlem2  15825  2sqlem3  15836