Theorem mulassd 11197

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

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

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

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

This theorem is referenced by:  recex  11810  mulcand  11811  receu  11823  divmulasscom  11861  divdivdiv  11883  divmuleq  11887  conjmul  11899  modmul1  13889  moddi  13904  expadd  14069  mulbinom2  14188  binom3  14189  digit1  14202  discr1  14204  discr  14205  faclbnd  14255  faclbnd6  14264  bcm1k  14280  bcp1nk  14282  crre  15080  remullem  15094  amgm2  15336  iseraltlem2  15649  iseraltlem3  15650  binomlem  15795  climcndslem2  15816  pwdif  15834  geo2sum  15839  mertenslem1  15850  clim2prod  15854  fallrisefac  15991  binomfallfaclem2  16006  bpolydiflem  16020  bpoly4  16025  sinadd  16132  tanadd  16135  pwp1fsum  16361  bezoutlem3  16511  dvdsmulgcd  16526  qredeq  16627  pcaddlem  16859  prmpwdvds  16875  ablfacrp  19998  nmoco  24625  cph2ass  25113  cphipval2  25141  csbren  25299  minveclem2  25326  uniioombllem5  25488  itg1mulc  25605  mbfi1fseqlem5  25620  itgconst  25720  itgmulc2  25735  dvexp  25857  dvply1  26191  elqaalem3  26229  aalioulem1  26240  aaliou3lem2  26251  dvtaylp  26278  dvradcnv  26330  pserdvlem2  26338  tangtx  26414  tanregt0  26448  tanarg  26528  logcnlem4  26554  cxpmul  26597  dvcxp1  26649  dvcncxp1  26652  root1eq1  26665  heron  26748  quad2  26749  dcubic1lem  26753  dcubic1  26755  cubic2  26758  binom4  26760  dquartlem1  26761  dquartlem2  26762  dquart  26763  quart1lem  26765  quart1  26766  quartlem1  26767  efiasin  26798  asinsinlem  26801  asinsin  26802  efiatan  26822  efiatan2  26827  2efiatan  26828  atantan  26833  atanbndlem  26835  atans2  26841  atantayl  26847  log2cnv  26854  log2tlbnd  26855  ftalem1  26983  ftalem5  26987  basellem3  26993  basellem5  26995  basellem8  26998  chtub  27123  perfectlem1  27140  perfectlem2  27141  perfect  27142  bcmono  27188  bclbnd  27191  bposlem9  27203  lgsneg  27232  gausslemma2dlem6  27283  lgseisenlem1  27286  lgseisenlem2  27287  lgseisenlem3  27288  lgseisenlem4  27289  lgsquad2lem1  27295  lgsquad3  27298  2lgslem3a  27307  2lgslem3b  27308  2lgslem3c  27309  2lgslem3d  27310  2lgsoddprmlem2  27320  2sqlem3  27331  chto1ub  27387  rplogsumlem1  27395  dchrmusum2  27405  dchrvmasum2lem  27407  dchrvmasumlem2  27409  dchrvmasumiflem2  27413  dchrisum0lem1  27427  dchrisum0lem2  27429  mulog2sumlem2  27446  chpdifbndlem1  27464  selberg3lem1  27468  selberg4lem1  27471  selberg34r  27482  pntrlog2bndlem3  27490  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntlemh  27510  pntlemr  27513  pntlemf  27516  pntlemk  27517  pntlemo  27518  colinearalglem4  28836  axpasch  28868  axcontlem2  28892  axcontlem4  28894  axcontlem7  28897  axcontlem8  28898  ipasslem4  30763  minvecolem2  30804  his35  31017  leopnmid  32067  quad3d  32673  zringfrac  33525  ccfldsrarelvec  33666  constrrtll  33721  constrrtlc1  33722  constrrtcclem  33724  constrrtcc  33725  cos9thpiminplylem2  33773  oddpwdc  34345  prodfzo03  34594  itgexpif  34597  breprexplemc  34623  circlemeth  34631  hgt750lemg  34645  hgt750lemb  34647  hgt750leme  34649  subfacval2  35174  subfaclim  35175  circum  35661  faclimlem1  35730  faclimlem3  35732  faclim2  35735  unbdqndv2lem1  36497  knoppndvlem2  36501  knoppndvlem7  36506  knoppndvlem11  36510  knoppndvlem12  36511  knoppndvlem14  36513  knoppndvlem18  36517  itgmulc2nc  37682  areacirclem1  37702  areacirclem4  37705  bfplem1  37816  lcmineqlem1  42017  lcmineqlem5  42021  lcmineqlem10  42026  lcmineqlem12  42028  lcmineqlem18  42034  lcmineqlem20  42036  dvrelogpow2b  42056  aks4d1p1p7  42062  primrootscoprmpow  42087  2np3bcnp1  42132  remulcan2d  42245  remul02  42393  remul01  42395  sn-it0e0  42404  remulinvcom  42421  remullid  42422  sn-mullid  42424  remulcand  42427  rediveud  42431  sn-0tie0  42439  sn-mul02  42440  mulgt0b1d  42460  mulgt0b2d  42466  mullt0b1d  42471  sn-itrere  42476  sn-retire  42477  flt4lem5e  42644  flt4lem5f  42645  fltnlta  42651  cu3addd  42669  3cubeslem2  42673  3cubeslem3l  42674  3cubeslem3r  42675  pellexlem6  42822  rmxluc  42925  rmyluc2  42927  rmydbl  42929  jm2.18  42977  jm2.23  42985  jm2.27c  42996  jm3.1lem2  43007  proot1ex  43185  sqrtcval  43630  sqrtcval2  43631  int-mulassocd  44166  binomcxplemnotnn0  44345  mul13d  45278  fmul01lt1lem1  45582  fmul01lt1lem2  45583  coskpi2  45864  cosknegpi  45867  dvnxpaek  45940  dvmptfprodlem  45942  dvnprodlem2  45945  itgsinexplem1  45952  stoweidlem26  46024  wallispilem5  46067  wallispi  46068  wallispi2lem1  46069  wallispi2lem2  46070  stirlinglem3  46074  stirlinglem10  46081  stirlinglem15  46086  dirkertrigeqlem1  46096  dirkertrigeqlem2  46097  dirkertrigeqlem3  46098  dirkertrigeq  46099  dirkercncflem2  46102  fourierdlem66  46170  fourierswlem  46228  fouriersw  46229  etransclem23  46255  etransclem25  46257  etransclem46  46278  hoidmvlelem2  46594  sigarls  46855  sharhght  46863  modmkpkne  47362  fmtnorec4  47550  fmtnoprmfac2lem1  47567  fmtnoprmfac2  47568  fmtnofac2lem  47569  fmtnofac1  47571  lighneallem4a  47609  perfectALTVlem1  47722  perfectALTVlem2  47723  perfectALTV  47724  2zrngmmgm  48240  altgsumbcALT  48341  nn0sumshdiglemB  48609  affinecomb2  48692  itscnhlc0yqe  48748  itschlc0yqe  48749  itsclc0yqsollem1  48751  itsclc0yqsol  48753  itscnhlc0xyqsol  48754  itsclc0xyqsolr  48758  itsclquadb  48765  aacllem  49790