Theorem mulass 8055

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1372   ∈ wcel 2175  (class class class)co 5943  ℂcc 7922   · cmul 7929

This theorem was proved from axioms:  ax-mulass 8027

This theorem is referenced by:  mulrid  8068  mulassi  8080  mulassd  8095  mul12  8200  mul32  8201  mul31  8202  mul4  8203  rimul  8657  divassap  8762  cju  9033  div4p1lem1div2  9290  mulbinom2  10799  sqoddm1div8  10836  remim  11113  imval2  11147  clim2divap  11793  prod3fmul  11794  prodmodclem3  11828  absefib  12024  efieq1re  12025  muldvds1  12069  muldvds2  12070  dvdsmulc  12072  dvdstr  12081  oddprmdvds  12619  cncrng  14273  abssinper  15260  2sqlem6  15539