Theorem mulassd 8045

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

Syntax hints:   -> wi 4   = wceq 1364   e. wcel 2164  (class class class)co 5919   CCcc 7872   x. cmul 7879

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 7977

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

This theorem is referenced by:  ltmul1  8613  recexap  8674  mulap0  8675  mulcanapd  8682  receuap  8690  divmulasscomap  8717  divdivdivap  8734  divmuleqap  8738  conjmulap  8750  apmul1  8809  qapne  9707  modqmul1  10451  modqdi  10466  expadd  10655  mulbinom2  10730  binom3  10731  faclbnd  10815  faclbnd6  10818  bcm1k  10834  bcp1nk  10836  bcval5  10837  crre  11004  remullem  11018  resqrexlemcalc1  11161  resqrexlemnm  11165  amgm2  11265  binomlem  11629  geo2sum  11660  mertenslemi1  11681  clim2prod  11685  sinadd  11882  tanaddap  11885  dvdsmulcr  11967  dvdsmulgcd  12165  qredeq  12237  2sqpwodd  12317  pcaddlem  12480  prmpwdvds  12496  dvexp  14890  dvply1  14943  tangtx  15014  cxpmul  15088  binom4  15152  lgsneg  15181  gausslemma2dlem6  15224  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisenlem4  15230  lgsquad2lem1  15238  lgsquad3  15241  2lgslem3a  15250  2lgslem3b  15251  2lgslem3c  15252  2lgslem3d  15253  2lgsoddprmlem2  15263  2sqlem3  15274