Theorem mulass 11105

Description: Alias for ax-mulass 11083, for naming consistency with mulassi 11134. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
mulass	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Proof of Theorem mulass

Step	Hyp	Ref	Expression
1		ax-mulass 11083	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  (class class class)co 7355  ℂcc 11015   · cmul 11022

This theorem was proved from axioms:  ax-mulass 11083

This theorem is referenced by:  mulrid  11121  mulassi  11134  mulassd  11146  mul12  11289  mul32  11290  mul31  11291  mul4  11292  00id  11299  divass  11805  cju  12132  div4p1lem1div2  12387  xmulasslem3  13192  mulbinom2  14137  sqoddm1div8  14157  faclbnd5  14212  bcval5  14232  remim  15031  imval2  15065  01sqrexlem7  15162  sqrtneglem  15180  sqreulem  15274  clim2div  15803  prodfmul  15804  prodmolem3  15847  sinhval  16070  coshval  16071  absefib  16114  efieq1re  16115  muldvds1  16198  muldvds2  16199  dvdsmulc  16201  dvdsmulcr  16203  dvdstr  16212  eulerthlem2  16700  oddprmdvds  16822  ablfacrp  19988  cncrng  21334  cncrngOLD  21335  nmoleub2lem3  25062  cnlmod  25087  itg2mulc  25695  abssinper  26477  sinasin  26846  dchrabl  27212  bposlem6  27247  bposlem9  27250  2sqlem6  27381  rpvmasum2  27470  cncvcOLD  30584  ipasslem5  30836  ipasslem11  30841  dvasin  37817  facp2  42309  pellexlem2  42987  jm2.25  43156  expgrowth  44492  2zrngmsgrp  48415  nn0sumshdiglemA  48781