Theorem mulass 7376

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 920   = wceq 1285   ∈ wcel 1434  (class class class)co 5591  ℂcc 7251   · cmul 7258

This theorem was proved from axioms:  ax-mulass 7351

This theorem is referenced by:  mulid1  7388  mulassi  7400  mulassd  7414  mul12  7514  mul32  7515  mul31  7516  mul4  7517  rimul  7962  divassap  8055  cju  8315  div4p1lem1div2  8561  mulbinom2  9905  sqoddm1div8  9941  remim  10121  imval2  10155  muldvds1  10601  muldvds2  10602  dvdsmulc  10604  dvdstr  10613