Theorem mulassd 11155

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   · cmul 11031

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

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

This theorem is referenced by:  recex  11769  mulcand  11770  receu  11782  divmulasscom  11820  divdivdiv  11842  divmuleq  11846  conjmul  11858  modmul1  13847  moddi  13862  expadd  14027  mulbinom2  14146  binom3  14147  digit1  14160  discr1  14162  discr  14163  faclbnd  14213  faclbnd6  14222  bcm1k  14238  bcp1nk  14240  crre  15037  remullem  15051  amgm2  15293  iseraltlem2  15606  iseraltlem3  15607  binomlem  15752  climcndslem2  15773  pwdif  15791  geo2sum  15796  mertenslem1  15807  clim2prod  15811  fallrisefac  15948  binomfallfaclem2  15963  bpolydiflem  15977  bpoly4  15982  sinadd  16089  tanadd  16092  pwp1fsum  16318  bezoutlem3  16468  dvdsmulgcd  16483  qredeq  16584  pcaddlem  16816  prmpwdvds  16832  ablfacrp  19997  nmoco  24681  cph2ass  25169  cphipval2  25197  csbren  25355  minveclem2  25382  uniioombllem5  25544  itg1mulc  25661  mbfi1fseqlem5  25676  itgconst  25776  itgmulc2  25791  dvexp  25913  dvply1  26247  elqaalem3  26285  aalioulem1  26296  aaliou3lem2  26307  dvtaylp  26334  dvradcnv  26386  pserdvlem2  26394  tangtx  26470  tanregt0  26504  tanarg  26584  logcnlem4  26610  cxpmul  26653  dvcxp1  26705  dvcncxp1  26708  root1eq1  26721  heron  26804  quad2  26805  dcubic1lem  26809  dcubic1  26811  cubic2  26814  binom4  26816  dquartlem1  26817  dquartlem2  26818  dquart  26819  quart1lem  26821  quart1  26822  quartlem1  26823  efiasin  26854  asinsinlem  26857  asinsin  26858  efiatan  26878  efiatan2  26883  2efiatan  26884  atantan  26889  atanbndlem  26891  atans2  26897  atantayl  26903  log2cnv  26910  log2tlbnd  26911  ftalem1  27039  ftalem5  27043  basellem3  27049  basellem5  27051  basellem8  27054  chtub  27179  perfectlem1  27196  perfectlem2  27197  perfect  27198  bcmono  27244  bclbnd  27247  bposlem9  27259  lgsneg  27288  gausslemma2dlem6  27339  lgseisenlem1  27342  lgseisenlem2  27343  lgseisenlem3  27344  lgseisenlem4  27345  lgsquad2lem1  27351  lgsquad3  27354  2lgslem3a  27363  2lgslem3b  27364  2lgslem3c  27365  2lgslem3d  27366  2lgsoddprmlem2  27376  2sqlem3  27387  chto1ub  27443  rplogsumlem1  27451  dchrmusum2  27461  dchrvmasum2lem  27463  dchrvmasumlem2  27465  dchrvmasumiflem2  27469  dchrisum0lem1  27483  dchrisum0lem2  27485  mulog2sumlem2  27502  chpdifbndlem1  27520  selberg3lem1  27524  selberg4lem1  27527  selberg34r  27538  pntrlog2bndlem3  27546  pntrlog2bndlem5  27548  pntrlog2bndlem6  27550  pntlemh  27566  pntlemr  27569  pntlemf  27572  pntlemk  27573  pntlemo  27574  colinearalglem4  28982  axpasch  29014  axcontlem2  29038  axcontlem4  29040  axcontlem7  29043  axcontlem8  29044  ipasslem4  30909  minvecolem2  30950  his35  31163  leopnmid  32213  quad3d  32829  zringfrac  33635  ccfldsrarelvec  33828  constrrtll  33888  constrrtlc1  33889  constrrtcclem  33891  constrrtcc  33892  cos9thpiminplylem2  33940  oddpwdc  34511  prodfzo03  34760  itgexpif  34763  breprexplemc  34789  circlemeth  34797  hgt750lemg  34811  hgt750lemb  34813  hgt750leme  34815  subfacval2  35381  subfaclim  35382  circum  35868  faclimlem1  35937  faclimlem3  35939  faclim2  35942  unbdqndv2lem1  36709  knoppndvlem2  36713  knoppndvlem7  36718  knoppndvlem11  36722  knoppndvlem12  36723  knoppndvlem14  36725  knoppndvlem18  36729  itgmulc2nc  37885  areacirclem1  37905  areacirclem4  37908  bfplem1  38019  lcmineqlem1  42279  lcmineqlem5  42283  lcmineqlem10  42288  lcmineqlem12  42290  lcmineqlem18  42296  lcmineqlem20  42298  dvrelogpow2b  42318  aks4d1p1p7  42324  primrootscoprmpow  42349  2np3bcnp1  42394  remulcan2d  42508  remul02  42656  remul01  42658  sn-it0e0  42667  remulinvcom  42684  remullid  42685  sn-mullid  42687  remulcand  42690  rediveud  42694  sn-0tie0  42702  sn-mul02  42703  mulgt0b1d  42723  mulgt0b2d  42729  mullt0b1d  42734  sn-itrere  42739  sn-retire  42740  flt4lem5e  42895  flt4lem5f  42896  fltnlta  42902  cu3addd  42919  3cubeslem2  42923  3cubeslem3l  42924  3cubeslem3r  42925  pellexlem6  43072  rmxluc  43174  rmyluc2  43176  rmydbl  43178  jm2.18  43226  jm2.23  43234  jm2.27c  43245  jm3.1lem2  43256  proot1ex  43434  sqrtcval  43878  sqrtcval2  43879  int-mulassocd  44414  binomcxplemnotnn0  44593  mul13d  45524  fmul01lt1lem1  45826  fmul01lt1lem2  45827  coskpi2  46106  cosknegpi  46109  dvnxpaek  46182  dvmptfprodlem  46184  dvnprodlem2  46187  itgsinexplem1  46194  stoweidlem26  46266  wallispilem5  46309  wallispi  46310  wallispi2lem1  46311  wallispi2lem2  46312  stirlinglem3  46316  stirlinglem10  46323  stirlinglem15  46328  dirkertrigeqlem1  46338  dirkertrigeqlem2  46339  dirkertrigeqlem3  46340  dirkertrigeq  46341  dirkercncflem2  46344  fourierdlem66  46412  fourierswlem  46470  fouriersw  46471  etransclem23  46497  etransclem25  46499  etransclem46  46520  hoidmvlelem2  46836  sigarls  47097  sharhght  47105  modmkpkne  47603  fmtnorec4  47791  fmtnoprmfac2lem1  47808  fmtnoprmfac2  47809  fmtnofac2lem  47810  fmtnofac1  47812  lighneallem4a  47850  perfectALTVlem1  47963  perfectALTVlem2  47964  perfectALTV  47965  2zrngmmgm  48494  altgsumbcALT  48595  nn0sumshdiglemB  48862  affinecomb2  48945  itscnhlc0yqe  49001  itschlc0yqe  49002  itsclc0yqsollem1  49004  itsclc0yqsol  49006  itscnhlc0xyqsol  49007  itsclc0xyqsolr  49011  itsclquadb  49018  aacllem  50042