Theorem mulass 11114

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

Assertion

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

Proof of Theorem mulass

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

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

This theorem was proved from axioms:  ax-mulass 11092

This theorem is referenced by:  mulrid  11130  mulassi  11143  mulassd  11155  mul12  11298  mul32  11299  mul31  11300  mul4  11301  00id  11308  divass  11814  cju  12141  div4p1lem1div2  12396  xmulasslem3  13201  mulbinom2  14146  sqoddm1div8  14166  faclbnd5  14221  bcval5  14241  remim  15040  imval2  15074  01sqrexlem7  15171  sqrtneglem  15189  sqreulem  15283  clim2div  15812  prodfmul  15813  prodmolem3  15856  sinhval  16079  coshval  16080  absefib  16123  efieq1re  16124  muldvds1  16207  muldvds2  16208  dvdsmulc  16210  dvdsmulcr  16212  dvdstr  16221  eulerthlem2  16709  oddprmdvds  16831  ablfacrp  19997  cncrng  21343  cncrngOLD  21344  nmoleub2lem3  25071  cnlmod  25096  itg2mulc  25704  abssinper  26486  sinasin  26855  dchrabl  27221  bposlem6  27256  bposlem9  27259  2sqlem6  27390  rpvmasum2  27479  cncvcOLD  30658  ipasslem5  30910  ipasslem11  30915  dvasin  37905  facp2  42397  pellexlem2  43072  jm2.25  43241  expgrowth  44576  2zrngmsgrp  48499  nn0sumshdiglemA  48865