Theorem mulassd 10063

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

Syntax hints:   -> wi 4   = wceq 1483   e. wcel 1990  (class class class)co 6650   CCcc 9934   x. cmul 9941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 10002

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  recex  10659  mulcand  10660  receu  10672  divmulasscom  10709  divdivdiv  10726  divmuleq  10730  conjmul  10742  modmul1  12723  moddi  12738  expadd  12902  mulbinom2  12984  binom3  12985  digit1  12998  discr1  13000  discr  13001  faclbnd  13077  faclbnd6  13086  bcm1k  13102  bcp1nk  13104  crre  13854  remullem  13868  amgm2  14109  iseraltlem2  14413  iseraltlem3  14414  binomlem  14561  climcndslem2  14582  geo2sum  14604  mertenslem1  14616  clim2prod  14620  fallrisefac  14756  binomfallfaclem2  14771  bpolydiflem  14785  bpoly4  14790  sinadd  14894  tanadd  14897  pwp1fsum  15114  bezoutlem3  15258  dvdsmulgcd  15274  qredeq  15371  pcaddlem  15592  prmpwdvds  15608  ablfacrp  18465  nmoco  22541  cph2ass  23013  cphipval2  23040  csbren  23182  minveclem2  23197  uniioombllem5  23355  itg1mulc  23471  mbfi1fseqlem5  23486  itgconst  23585  itgmulc2  23600  dvexp  23716  dvply1  24039  elqaalem3  24076  aalioulem1  24087  aaliou3lem2  24098  dvtaylp  24124  dvradcnv  24175  pserdvlem2  24182  tangtx  24257  tanregt0  24285  tanarg  24365  logcnlem4  24391  cxpmul  24434  dvcxp1  24481  dvcncxp1  24484  root1eq1  24496  heron  24565  quad2  24566  dcubic1lem  24570  dcubic1  24572  cubic2  24575  binom4  24577  dquartlem1  24578  dquartlem2  24579  dquart  24580  quart1lem  24582  quart1  24583  quartlem1  24584  efiasin  24615  asinsinlem  24618  asinsin  24619  efiatan  24639  efiatan2  24644  2efiatan  24645  atantan  24650  atanbndlem  24652  atans2  24658  atantayl  24664  log2cnv  24671  log2tlbnd  24672  ftalem1  24799  ftalem5  24803  basellem3  24809  basellem5  24811  basellem8  24814  chtub  24937  perfectlem1  24954  perfectlem2  24955  perfect  24956  bcmono  25002  bclbnd  25005  bposlem9  25017  lgsneg  25046  gausslemma2dlem6  25097  lgseisenlem1  25100  lgseisenlem2  25101  lgseisenlem3  25102  lgseisenlem4  25103  lgsquad2lem1  25109  lgsquad3  25112  2lgslem3a  25121  2lgslem3b  25122  2lgslem3c  25123  2lgslem3d  25124  2lgsoddprmlem2  25134  2sqlem3  25145  chto1ub  25165  rplogsumlem1  25173  dchrmusum2  25183  dchrvmasum2lem  25185  dchrvmasumlem2  25187  dchrvmasumiflem2  25191  dchrisum0lem1  25205  dchrisum0lem2  25207  mulog2sumlem2  25224  chpdifbndlem1  25242  selberg3lem1  25246  selberg4lem1  25249  selberg34r  25260  pntrlog2bndlem3  25268  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntlemh  25288  pntlemr  25291  pntlemf  25294  pntlemk  25295  pntlemo  25296  colinearalglem4  25789  axpasch  25821  axcontlem2  25845  axcontlem4  25847  axcontlem7  25850  axcontlem8  25851  ipasslem4  27689  minvecolem2  27731  his35  27945  leopnmid  28997  oddpwdc  30416  prodfzo03  30681  itgexpif  30684  breprexplemc  30710  circlemeth  30718  hgt750lemg  30732  hgt750lemb  30734  hgt750leme  30736  subfacval2  31169  subfaclim  31170  circum  31568  faclimlem1  31629  faclimlem3  31631  faclim2  31634  unbdqndv2lem1  32500  knoppndvlem2  32504  knoppndvlem7  32509  knoppndvlem11  32513  knoppndvlem12  32514  knoppndvlem14  32516  knoppndvlem18  32520  itgmulc2nc  33478  areacirclem1  33500  areacirclem4  33503  bfplem1  33621  pellexlem6  37398  rmxluc  37501  rmyluc2  37503  rmydbl  37505  jm2.18  37555  jm2.23  37563  jm2.27c  37574  jm3.1lem2  37585  proot1ex  37779  int-mulassocd  38480  binomcxplemnotnn0  38555  mul13d  39491  fmul01lt1lem1  39816  fmul01lt1lem2  39817  coskpi2  40077  cosknegpi  40080  dvnxpaek  40157  dvmptfprodlem  40159  dvnprodlem2  40162  itgsinexplem1  40169  stoweidlem26  40243  wallispilem5  40286  wallispi  40287  wallispi2lem1  40288  wallispi2lem2  40289  stirlinglem3  40293  stirlinglem10  40300  stirlinglem15  40305  dirkertrigeqlem1  40315  dirkertrigeqlem2  40316  dirkertrigeqlem3  40317  dirkertrigeq  40318  dirkercncflem2  40321  fourierdlem66  40389  fourierswlem  40447  fouriersw  40448  etransclem23  40474  etransclem25  40476  etransclem46  40497  hoidmvlelem2  40810  sigarls  41046  sharhght  41054  fmtnorec4  41461  fmtnoprmfac2lem1  41478  fmtnoprmfac2  41479  fmtnofac2lem  41480  fmtnofac1  41482  pwdif  41501  lighneallem4a  41525  perfectALTVlem1  41630  perfectALTVlem2  41631  perfectALTV  41632  2zrngmmgm  41946  altgsumbcALT  42131  nn0sumshdiglemB  42414  aacllem  42547