Theorem mulass 7775

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 963   = wceq 1332   ∈ wcel 1481  (class class class)co 5782  ℂcc 7642   · cmul 7649

This theorem was proved from axioms:  ax-mulass 7747

This theorem is referenced by:  mulid1  7787  mulassi  7799  mulassd  7813  mul12  7915  mul32  7916  mul31  7917  mul4  7918  rimul  8371  divassap  8474  cju  8743  div4p1lem1div2  8997  mulbinom2  10439  sqoddm1div8  10475  remim  10664  imval2  10698  clim2divap  11341  prod3fmul  11342  prodmodclem3  11376  absefib  11513  efieq1re  11514  muldvds1  11554  muldvds2  11555  dvdsmulc  11557  dvdstr  11566  abssinper  12975