Theorem mulassd 11256

Description: Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
addcld.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
addcld.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
addassd.3	⊢ (𝜑 → 𝐶 ∈ ℂ)

Assertion

Ref	Expression
mulassd	⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Proof of Theorem mulassd

Step	Hyp	Ref	Expression
1		addcld.1	. 2 ⊢ (𝜑 → 𝐴 ∈ ℂ)
2		addcld.2	. 2 ⊢ (𝜑 → 𝐵 ∈ ℂ)
3		addassd.3	. 2 ⊢ (𝜑 → 𝐶 ∈ ℂ)
4		mulass 11215	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  (class class class)co 7403  ℂcc 11125   · cmul 11132

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  recex  11867  mulcand  11868  receu  11880  divmulasscom  11918  divdivdiv  11940  divmuleq  11944  conjmul  11956  modmul1  13940  moddi  13955  expadd  14120  mulbinom2  14239  binom3  14240  digit1  14253  discr1  14255  discr  14256  faclbnd  14306  faclbnd6  14315  bcm1k  14331  bcp1nk  14333  crre  15131  remullem  15145  amgm2  15386  iseraltlem2  15697  iseraltlem3  15698  binomlem  15843  climcndslem2  15864  pwdif  15882  geo2sum  15887  mertenslem1  15898  clim2prod  15902  fallrisefac  16039  binomfallfaclem2  16054  bpolydiflem  16068  bpoly4  16073  sinadd  16180  tanadd  16183  pwp1fsum  16408  bezoutlem3  16558  dvdsmulgcd  16573  qredeq  16674  pcaddlem  16906  prmpwdvds  16922  ablfacrp  20047  nmoco  24674  cph2ass  25163  cphipval2  25191  csbren  25349  minveclem2  25376  uniioombllem5  25538  itg1mulc  25655  mbfi1fseqlem5  25670  itgconst  25770  itgmulc2  25785  dvexp  25907  dvply1  26241  elqaalem3  26279  aalioulem1  26290  aaliou3lem2  26301  dvtaylp  26328  dvradcnv  26380  pserdvlem2  26388  tangtx  26464  tanregt0  26498  tanarg  26578  logcnlem4  26604  cxpmul  26647  dvcxp1  26699  dvcncxp1  26702  root1eq1  26715  heron  26798  quad2  26799  dcubic1lem  26803  dcubic1  26805  cubic2  26808  binom4  26810  dquartlem1  26811  dquartlem2  26812  dquart  26813  quart1lem  26815  quart1  26816  quartlem1  26817  efiasin  26848  asinsinlem  26851  asinsin  26852  efiatan  26872  efiatan2  26877  2efiatan  26878  atantan  26883  atanbndlem  26885  atans2  26891  atantayl  26897  log2cnv  26904  log2tlbnd  26905  ftalem1  27033  ftalem5  27037  basellem3  27043  basellem5  27045  basellem8  27048  chtub  27173  perfectlem1  27190  perfectlem2  27191  perfect  27192  bcmono  27238  bclbnd  27241  bposlem9  27253  lgsneg  27282  gausslemma2dlem6  27333  lgseisenlem1  27336  lgseisenlem2  27337  lgseisenlem3  27338  lgseisenlem4  27339  lgsquad2lem1  27345  lgsquad3  27348  2lgslem3a  27357  2lgslem3b  27358  2lgslem3c  27359  2lgslem3d  27360  2lgsoddprmlem2  27370  2sqlem3  27381  chto1ub  27437  rplogsumlem1  27445  dchrmusum2  27455  dchrvmasum2lem  27457  dchrvmasumlem2  27459  dchrvmasumiflem2  27463  dchrisum0lem1  27477  dchrisum0lem2  27479  mulog2sumlem2  27496  chpdifbndlem1  27514  selberg3lem1  27518  selberg4lem1  27521  selberg34r  27532  pntrlog2bndlem3  27540  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntlemh  27560  pntlemr  27563  pntlemf  27566  pntlemk  27567  pntlemo  27568  colinearalglem4  28834  axpasch  28866  axcontlem2  28890  axcontlem4  28892  axcontlem7  28895  axcontlem8  28896  ipasslem4  30761  minvecolem2  30802  his35  31015  leopnmid  32065  quad3d  32673  zringfrac  33515  ccfldsrarelvec  33658  constrrtll  33711  constrrtlc1  33712  constrrtcclem  33714  constrrtcc  33715  cos9thpiminplylem2  33763  oddpwdc  34332  prodfzo03  34581  itgexpif  34584  breprexplemc  34610  circlemeth  34618  hgt750lemg  34632  hgt750lemb  34634  hgt750leme  34636  subfacval2  35155  subfaclim  35156  circum  35642  faclimlem1  35706  faclimlem3  35708  faclim2  35711  unbdqndv2lem1  36473  knoppndvlem2  36477  knoppndvlem7  36482  knoppndvlem11  36486  knoppndvlem12  36487  knoppndvlem14  36489  knoppndvlem18  36493  itgmulc2nc  37658  areacirclem1  37678  areacirclem4  37681  bfplem1  37792  lcmineqlem1  41988  lcmineqlem5  41992  lcmineqlem10  41997  lcmineqlem12  41999  lcmineqlem18  42005  lcmineqlem20  42007  dvrelogpow2b  42027  aks4d1p1p7  42033  primrootscoprmpow  42058  2np3bcnp1  42103  remulcan2d  42255  remul02  42395  remul01  42397  sn-it0e0  42405  remulinvcom  42422  remullid  42423  sn-mullid  42425  remulcand  42428  sn-0tie0  42429  sn-mul02  42430  mulgt0b2d  42450  sn-itrere  42458  sn-retire  42459  flt4lem5e  42626  flt4lem5f  42627  fltnlta  42633  cu3addd  42651  3cubeslem2  42655  3cubeslem3l  42656  3cubeslem3r  42657  pellexlem6  42804  rmxluc  42907  rmyluc2  42909  rmydbl  42911  jm2.18  42959  jm2.23  42967  jm2.27c  42978  jm3.1lem2  42989  proot1ex  43167  sqrtcval  43612  sqrtcval2  43613  int-mulassocd  44148  binomcxplemnotnn0  44328  mul13d  45256  fmul01lt1lem1  45561  fmul01lt1lem2  45562  coskpi2  45843  cosknegpi  45846  dvnxpaek  45919  dvmptfprodlem  45921  dvnprodlem2  45924  itgsinexplem1  45931  stoweidlem26  46003  wallispilem5  46046  wallispi  46047  wallispi2lem1  46048  wallispi2lem2  46049  stirlinglem3  46053  stirlinglem10  46060  stirlinglem15  46065  dirkertrigeqlem1  46075  dirkertrigeqlem2  46076  dirkertrigeqlem3  46077  dirkertrigeq  46078  dirkercncflem2  46081  fourierdlem66  46149  fourierswlem  46207  fouriersw  46208  etransclem23  46234  etransclem25  46236  etransclem46  46257  hoidmvlelem2  46573  sigarls  46834  sharhght  46842  fmtnorec4  47511  fmtnoprmfac2lem1  47528  fmtnoprmfac2  47529  fmtnofac2lem  47530  fmtnofac1  47532  lighneallem4a  47570  perfectALTVlem1  47683  perfectALTVlem2  47684  perfectALTV  47685  2zrngmmgm  48175  altgsumbcALT  48276  nn0sumshdiglemB  48548  affinecomb2  48631  itscnhlc0yqe  48687  itschlc0yqe  48688  itsclc0yqsollem1  48690  itsclc0yqsol  48692  itscnhlc0xyqsol  48693  itsclc0xyqsolr  48697  itsclquadb  48704  aacllem  49613