Theorem mulass 11272

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1537   ∈ wcel 2108  (class class class)co 7448  ℂcc 11182   · cmul 11189

This theorem was proved from axioms:  ax-mulass 11250

This theorem is referenced by:  mulrid  11288  mulassi  11301  mulassd  11313  mul12  11455  mul32  11456  mul31  11457  mul4  11458  00id  11465  divass  11967  cju  12289  div4p1lem1div2  12548  xmulasslem3  13348  mulbinom2  14272  sqoddm1div8  14292  faclbnd5  14347  bcval5  14367  remim  15166  imval2  15200  01sqrexlem7  15297  sqrtneglem  15315  sqreulem  15408  clim2div  15937  prodfmul  15938  prodmolem3  15981  sinhval  16202  coshval  16203  absefib  16246  efieq1re  16247  muldvds1  16329  muldvds2  16330  dvdsmulc  16332  dvdsmulcr  16334  dvdstr  16342  eulerthlem2  16829  oddprmdvds  16950  ablfacrp  20110  cncrng  21424  cncrngOLD  21425  nmoleub2lem3  25167  cnlmod  25192  itg2mulc  25802  abssinper  26581  sinasin  26950  dchrabl  27316  bposlem6  27351  bposlem9  27354  2sqlem6  27485  rpvmasum2  27574  cncvcOLD  30615  ipasslem5  30867  ipasslem11  30872  dvasin  37664  facp2  42100  fac2xp3  42196  pellexlem2  42786  jm2.25  42956  expgrowth  44304  2zrngmsgrp  47976  nn0sumshdiglemA  48353