Theorem mulass 8153

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1002   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8020   · cmul 8027

This theorem was proved from axioms:  ax-mulass 8125

This theorem is referenced by:  mulrid  8166  mulassi  8178  mulassd  8193  mul12  8298  mul32  8299  mul31  8300  mul4  8301  rimul  8755  divassap  8860  cju  9131  div4p1lem1div2  9388  mulbinom2  10908  sqoddm1div8  10945  remim  11411  imval2  11445  clim2divap  12091  prod3fmul  12092  prodmodclem3  12126  absefib  12322  efieq1re  12323  muldvds1  12367  muldvds2  12368  dvdsmulc  12370  dvdstr  12379  oddprmdvds  12917  cncrng  14573  abssinper  15560  2sqlem6  15839