Theorem mulass 11244

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  (class class class)co 7432  ℂcc 11154   · cmul 11161

This theorem was proved from axioms:  ax-mulass 11222

This theorem is referenced by:  mulrid  11260  mulassi  11273  mulassd  11285  mul12  11427  mul32  11428  mul31  11429  mul4  11430  00id  11437  divass  11941  cju  12263  div4p1lem1div2  12523  xmulasslem3  13329  mulbinom2  14263  sqoddm1div8  14283  faclbnd5  14338  bcval5  14358  remim  15157  imval2  15191  01sqrexlem7  15288  sqrtneglem  15306  sqreulem  15399  clim2div  15926  prodfmul  15927  prodmolem3  15970  sinhval  16191  coshval  16192  absefib  16235  efieq1re  16236  muldvds1  16319  muldvds2  16320  dvdsmulc  16322  dvdsmulcr  16324  dvdstr  16332  eulerthlem2  16820  oddprmdvds  16942  ablfacrp  20087  cncrng  21402  cncrngOLD  21403  nmoleub2lem3  25149  cnlmod  25174  itg2mulc  25783  abssinper  26564  sinasin  26933  dchrabl  27299  bposlem6  27334  bposlem9  27337  2sqlem6  27468  rpvmasum2  27557  cncvcOLD  30603  ipasslem5  30855  ipasslem11  30860  dvasin  37712  facp2  42145  fac2xp3  42241  pellexlem2  42846  jm2.25  43016  expgrowth  44359  2zrngmsgrp  48174  nn0sumshdiglemA  48545