Theorem mulass 8274

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1005   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   · cmul 8148

This theorem was proved from axioms:  ax-mulass 8246

This theorem is referenced by:  mulrid  8287  mulassi  8299  mulassd  8313  mul12  8418  mul32  8419  mul31  8420  mul4  8421  rimul  8876  divassap  8981  cju  9252  div4p1lem1div2  9509  mulbinom2  11042  sqoddm1div8  11080  remim  11570  imval2  11604  clim2divap  12251  prod3fmul  12252  prodmodclem3  12286  absefib  12482  efieq1re  12483  muldvds1  12527  muldvds2  12528  dvdsmulc  12530  dvdstr  12539  oddprmdvds  13077  cncrng  14843  abssinper  15837  pellexlem2  15972  2sqlem6  16119