Theorem mulassd 7983

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

Syntax hints:   -> wi 4   = wceq 1353   e. wcel 2148  (class class class)co 5877   CCcc 7811   x. cmul 7818

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 7916

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

This theorem is referenced by:  ltmul1  8551  recexap  8612  mulap0  8613  mulcanapd  8620  receuap  8628  divmulasscomap  8655  divdivdivap  8672  divmuleqap  8676  conjmulap  8688  apmul1  8747  qapne  9641  modqmul1  10379  modqdi  10394  expadd  10564  mulbinom2  10639  binom3  10640  faclbnd  10723  faclbnd6  10726  bcm1k  10742  bcp1nk  10744  bcval5  10745  crre  10868  remullem  10882  resqrexlemcalc1  11025  resqrexlemnm  11029  amgm2  11129  binomlem  11493  geo2sum  11524  mertenslemi1  11545  clim2prod  11549  sinadd  11746  tanaddap  11749  dvdsmulcr  11830  dvdsmulgcd  12028  qredeq  12098  2sqpwodd  12178  pcaddlem  12340  prmpwdvds  12355  dvexp  14214  tangtx  14298  cxpmul  14372  binom4  14436  lgsneg  14464  lgseisenlem1  14489  lgseisenlem2  14490  2lgsoddprmlem2  14493  2sqlem3  14503