Theorem mulass 11240

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   · cmul 11157

This theorem was proved from axioms:  ax-mulass 11218

This theorem is referenced by:  mulrid  11256  mulassi  11269  mulassd  11281  mul12  11423  mul32  11424  mul31  11425  mul4  11426  00id  11433  divass  11937  cju  12259  div4p1lem1div2  12518  xmulasslem3  13324  mulbinom2  14258  sqoddm1div8  14278  faclbnd5  14333  bcval5  14353  remim  15152  imval2  15186  01sqrexlem7  15283  sqrtneglem  15301  sqreulem  15394  clim2div  15921  prodfmul  15922  prodmolem3  15965  sinhval  16186  coshval  16187  absefib  16230  efieq1re  16231  muldvds1  16314  muldvds2  16315  dvdsmulc  16317  dvdsmulcr  16319  dvdstr  16327  eulerthlem2  16815  oddprmdvds  16936  ablfacrp  20100  cncrng  21418  cncrngOLD  21419  nmoleub2lem3  25161  cnlmod  25186  itg2mulc  25796  abssinper  26577  sinasin  26946  dchrabl  27312  bposlem6  27347  bposlem9  27350  2sqlem6  27481  rpvmasum2  27570  cncvcOLD  30611  ipasslem5  30863  ipasslem11  30868  dvasin  37690  facp2  42124  fac2xp3  42220  pellexlem2  42817  jm2.25  42987  expgrowth  44330  2zrngmsgrp  48096  nn0sumshdiglemA  48468