Theorem mulassd 11204

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 11163	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	syl3anc 1373	1 ⊢ (𝜑 → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   · cmul 11080

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

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

This theorem is referenced by:  recex  11817  mulcand  11818  receu  11830  divmulasscom  11868  divdivdiv  11890  divmuleq  11894  conjmul  11906  modmul1  13896  moddi  13911  expadd  14076  mulbinom2  14195  binom3  14196  digit1  14209  discr1  14211  discr  14212  faclbnd  14262  faclbnd6  14271  bcm1k  14287  bcp1nk  14289  crre  15087  remullem  15101  amgm2  15343  iseraltlem2  15656  iseraltlem3  15657  binomlem  15802  climcndslem2  15823  pwdif  15841  geo2sum  15846  mertenslem1  15857  clim2prod  15861  fallrisefac  15998  binomfallfaclem2  16013  bpolydiflem  16027  bpoly4  16032  sinadd  16139  tanadd  16142  pwp1fsum  16368  bezoutlem3  16518  dvdsmulgcd  16533  qredeq  16634  pcaddlem  16866  prmpwdvds  16882  ablfacrp  20005  nmoco  24632  cph2ass  25120  cphipval2  25148  csbren  25306  minveclem2  25333  uniioombllem5  25495  itg1mulc  25612  mbfi1fseqlem5  25627  itgconst  25727  itgmulc2  25742  dvexp  25864  dvply1  26198  elqaalem3  26236  aalioulem1  26247  aaliou3lem2  26258  dvtaylp  26285  dvradcnv  26337  pserdvlem2  26345  tangtx  26421  tanregt0  26455  tanarg  26535  logcnlem4  26561  cxpmul  26604  dvcxp1  26656  dvcncxp1  26659  root1eq1  26672  heron  26755  quad2  26756  dcubic1lem  26760  dcubic1  26762  cubic2  26765  binom4  26767  dquartlem1  26768  dquartlem2  26769  dquart  26770  quart1lem  26772  quart1  26773  quartlem1  26774  efiasin  26805  asinsinlem  26808  asinsin  26809  efiatan  26829  efiatan2  26834  2efiatan  26835  atantan  26840  atanbndlem  26842  atans2  26848  atantayl  26854  log2cnv  26861  log2tlbnd  26862  ftalem1  26990  ftalem5  26994  basellem3  27000  basellem5  27002  basellem8  27005  chtub  27130  perfectlem1  27147  perfectlem2  27148  perfect  27149  bcmono  27195  bclbnd  27198  bposlem9  27210  lgsneg  27239  gausslemma2dlem6  27290  lgseisenlem1  27293  lgseisenlem2  27294  lgseisenlem3  27295  lgseisenlem4  27296  lgsquad2lem1  27302  lgsquad3  27305  2lgslem3a  27314  2lgslem3b  27315  2lgslem3c  27316  2lgslem3d  27317  2lgsoddprmlem2  27327  2sqlem3  27338  chto1ub  27394  rplogsumlem1  27402  dchrmusum2  27412  dchrvmasum2lem  27414  dchrvmasumlem2  27416  dchrvmasumiflem2  27420  dchrisum0lem1  27434  dchrisum0lem2  27436  mulog2sumlem2  27453  chpdifbndlem1  27471  selberg3lem1  27475  selberg4lem1  27478  selberg34r  27489  pntrlog2bndlem3  27497  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntlemh  27517  pntlemr  27520  pntlemf  27523  pntlemk  27524  pntlemo  27525  colinearalglem4  28843  axpasch  28875  axcontlem2  28899  axcontlem4  28901  axcontlem7  28904  axcontlem8  28905  ipasslem4  30770  minvecolem2  30811  his35  31024  leopnmid  32074  quad3d  32680  zringfrac  33532  ccfldsrarelvec  33673  constrrtll  33728  constrrtlc1  33729  constrrtcclem  33731  constrrtcc  33732  cos9thpiminplylem2  33780  oddpwdc  34352  prodfzo03  34601  itgexpif  34604  breprexplemc  34630  circlemeth  34638  hgt750lemg  34652  hgt750lemb  34654  hgt750leme  34656  subfacval2  35181  subfaclim  35182  circum  35668  faclimlem1  35737  faclimlem3  35739  faclim2  35742  unbdqndv2lem1  36504  knoppndvlem2  36508  knoppndvlem7  36513  knoppndvlem11  36517  knoppndvlem12  36518  knoppndvlem14  36520  knoppndvlem18  36524  itgmulc2nc  37689  areacirclem1  37709  areacirclem4  37712  bfplem1  37823  lcmineqlem1  42024  lcmineqlem5  42028  lcmineqlem10  42033  lcmineqlem12  42035  lcmineqlem18  42041  lcmineqlem20  42043  dvrelogpow2b  42063  aks4d1p1p7  42069  primrootscoprmpow  42094  2np3bcnp1  42139  remulcan2d  42252  remul02  42400  remul01  42402  sn-it0e0  42411  remulinvcom  42428  remullid  42429  sn-mullid  42431  remulcand  42434  rediveud  42438  sn-0tie0  42446  sn-mul02  42447  mulgt0b1d  42467  mulgt0b2d  42473  mullt0b1d  42478  sn-itrere  42483  sn-retire  42484  flt4lem5e  42651  flt4lem5f  42652  fltnlta  42658  cu3addd  42676  3cubeslem2  42680  3cubeslem3l  42681  3cubeslem3r  42682  pellexlem6  42829  rmxluc  42932  rmyluc2  42934  rmydbl  42936  jm2.18  42984  jm2.23  42992  jm2.27c  43003  jm3.1lem2  43014  proot1ex  43192  sqrtcval  43637  sqrtcval2  43638  int-mulassocd  44173  binomcxplemnotnn0  44352  mul13d  45285  fmul01lt1lem1  45589  fmul01lt1lem2  45590  coskpi2  45871  cosknegpi  45874  dvnxpaek  45947  dvmptfprodlem  45949  dvnprodlem2  45952  itgsinexplem1  45959  stoweidlem26  46031  wallispilem5  46074  wallispi  46075  wallispi2lem1  46076  wallispi2lem2  46077  stirlinglem3  46081  stirlinglem10  46088  stirlinglem15  46093  dirkertrigeqlem1  46103  dirkertrigeqlem2  46104  dirkertrigeqlem3  46105  dirkertrigeq  46106  dirkercncflem2  46109  fourierdlem66  46177  fourierswlem  46235  fouriersw  46236  etransclem23  46262  etransclem25  46264  etransclem46  46285  hoidmvlelem2  46601  sigarls  46862  sharhght  46870  modmkpkne  47366  fmtnorec4  47554  fmtnoprmfac2lem1  47571  fmtnoprmfac2  47572  fmtnofac2lem  47573  fmtnofac1  47575  lighneallem4a  47613  perfectALTVlem1  47726  perfectALTVlem2  47727  perfectALTV  47728  2zrngmmgm  48244  altgsumbcALT  48345  nn0sumshdiglemB  48613  affinecomb2  48696  itscnhlc0yqe  48752  itschlc0yqe  48753  itsclc0yqsollem1  48755  itsclc0yqsol  48757  itscnhlc0xyqsol  48758  itsclc0xyqsolr  48762  itsclquadb  48769  aacllem  49794