Theorem mulassd 11132

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  (class class class)co 7346  ℂcc 11001   · cmul 11008

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

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

This theorem is referenced by:  recex  11746  mulcand  11747  receu  11759  divmulasscom  11797  divdivdiv  11819  divmuleq  11823  conjmul  11835  modmul1  13828  moddi  13843  expadd  14008  mulbinom2  14127  binom3  14128  digit1  14141  discr1  14143  discr  14144  faclbnd  14194  faclbnd6  14203  bcm1k  14219  bcp1nk  14221  crre  15018  remullem  15032  amgm2  15274  iseraltlem2  15587  iseraltlem3  15588  binomlem  15733  climcndslem2  15754  pwdif  15772  geo2sum  15777  mertenslem1  15788  clim2prod  15792  fallrisefac  15929  binomfallfaclem2  15944  bpolydiflem  15958  bpoly4  15963  sinadd  16070  tanadd  16073  pwp1fsum  16299  bezoutlem3  16449  dvdsmulgcd  16464  qredeq  16565  pcaddlem  16797  prmpwdvds  16813  ablfacrp  19978  nmoco  24650  cph2ass  25138  cphipval2  25166  csbren  25324  minveclem2  25351  uniioombllem5  25513  itg1mulc  25630  mbfi1fseqlem5  25645  itgconst  25745  itgmulc2  25760  dvexp  25882  dvply1  26216  elqaalem3  26254  aalioulem1  26265  aaliou3lem2  26276  dvtaylp  26303  dvradcnv  26355  pserdvlem2  26363  tangtx  26439  tanregt0  26473  tanarg  26553  logcnlem4  26579  cxpmul  26622  dvcxp1  26674  dvcncxp1  26677  root1eq1  26690  heron  26773  quad2  26774  dcubic1lem  26778  dcubic1  26780  cubic2  26783  binom4  26785  dquartlem1  26786  dquartlem2  26787  dquart  26788  quart1lem  26790  quart1  26791  quartlem1  26792  efiasin  26823  asinsinlem  26826  asinsin  26827  efiatan  26847  efiatan2  26852  2efiatan  26853  atantan  26858  atanbndlem  26860  atans2  26866  atantayl  26872  log2cnv  26879  log2tlbnd  26880  ftalem1  27008  ftalem5  27012  basellem3  27018  basellem5  27020  basellem8  27023  chtub  27148  perfectlem1  27165  perfectlem2  27166  perfect  27167  bcmono  27213  bclbnd  27216  bposlem9  27228  lgsneg  27257  gausslemma2dlem6  27308  lgseisenlem1  27311  lgseisenlem2  27312  lgseisenlem3  27313  lgseisenlem4  27314  lgsquad2lem1  27320  lgsquad3  27323  2lgslem3a  27332  2lgslem3b  27333  2lgslem3c  27334  2lgslem3d  27335  2lgsoddprmlem2  27345  2sqlem3  27356  chto1ub  27412  rplogsumlem1  27420  dchrmusum2  27430  dchrvmasum2lem  27432  dchrvmasumlem2  27434  dchrvmasumiflem2  27438  dchrisum0lem1  27452  dchrisum0lem2  27454  mulog2sumlem2  27471  chpdifbndlem1  27489  selberg3lem1  27493  selberg4lem1  27496  selberg34r  27507  pntrlog2bndlem3  27515  pntrlog2bndlem5  27517  pntrlog2bndlem6  27519  pntlemh  27535  pntlemr  27538  pntlemf  27541  pntlemk  27542  pntlemo  27543  colinearalglem4  28885  axpasch  28917  axcontlem2  28941  axcontlem4  28943  axcontlem7  28946  axcontlem8  28947  ipasslem4  30809  minvecolem2  30850  his35  31063  leopnmid  32113  quad3d  32728  zringfrac  33514  ccfldsrarelvec  33679  constrrtll  33739  constrrtlc1  33740  constrrtcclem  33742  constrrtcc  33743  cos9thpiminplylem2  33791  oddpwdc  34362  prodfzo03  34611  itgexpif  34614  breprexplemc  34640  circlemeth  34648  hgt750lemg  34662  hgt750lemb  34664  hgt750leme  34666  subfacval2  35219  subfaclim  35220  circum  35706  faclimlem1  35775  faclimlem3  35777  faclim2  35780  unbdqndv2lem1  36542  knoppndvlem2  36546  knoppndvlem7  36551  knoppndvlem11  36555  knoppndvlem12  36556  knoppndvlem14  36558  knoppndvlem18  36562  itgmulc2nc  37727  areacirclem1  37747  areacirclem4  37750  bfplem1  37861  lcmineqlem1  42061  lcmineqlem5  42065  lcmineqlem10  42070  lcmineqlem12  42072  lcmineqlem18  42078  lcmineqlem20  42080  dvrelogpow2b  42100  aks4d1p1p7  42106  primrootscoprmpow  42131  2np3bcnp1  42176  remulcan2d  42289  remul02  42437  remul01  42439  sn-it0e0  42448  remulinvcom  42465  remullid  42466  sn-mullid  42468  remulcand  42471  rediveud  42475  sn-0tie0  42483  sn-mul02  42484  mulgt0b1d  42504  mulgt0b2d  42510  mullt0b1d  42515  sn-itrere  42520  sn-retire  42521  flt4lem5e  42688  flt4lem5f  42689  fltnlta  42695  cu3addd  42713  3cubeslem2  42717  3cubeslem3l  42718  3cubeslem3r  42719  pellexlem6  42866  rmxluc  42968  rmyluc2  42970  rmydbl  42972  jm2.18  43020  jm2.23  43028  jm2.27c  43039  jm3.1lem2  43050  proot1ex  43228  sqrtcval  43673  sqrtcval2  43674  int-mulassocd  44209  binomcxplemnotnn0  44388  mul13d  45320  fmul01lt1lem1  45623  fmul01lt1lem2  45624  coskpi2  45903  cosknegpi  45906  dvnxpaek  45979  dvmptfprodlem  45981  dvnprodlem2  45984  itgsinexplem1  45991  stoweidlem26  46063  wallispilem5  46106  wallispi  46107  wallispi2lem1  46108  wallispi2lem2  46109  stirlinglem3  46113  stirlinglem10  46120  stirlinglem15  46125  dirkertrigeqlem1  46135  dirkertrigeqlem2  46136  dirkertrigeqlem3  46137  dirkertrigeq  46138  dirkercncflem2  46141  fourierdlem66  46209  fourierswlem  46267  fouriersw  46268  etransclem23  46294  etransclem25  46296  etransclem46  46317  hoidmvlelem2  46633  sigarls  46894  sharhght  46902  modmkpkne  47391  fmtnorec4  47579  fmtnoprmfac2lem1  47596  fmtnoprmfac2  47597  fmtnofac2lem  47598  fmtnofac1  47600  lighneallem4a  47638  perfectALTVlem1  47751  perfectALTVlem2  47752  perfectALTV  47753  2zrngmmgm  48282  altgsumbcALT  48383  nn0sumshdiglemB  48651  affinecomb2  48734  itscnhlc0yqe  48790  itschlc0yqe  48791  itsclc0yqsollem1  48793  itsclc0yqsol  48795  itscnhlc0xyqsol  48796  itsclc0xyqsolr  48800  itsclquadb  48807  aacllem  49832