Theorem mulass 8005

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2164  (class class class)co 5919  ℂcc 7872   · cmul 7879

This theorem was proved from axioms:  ax-mulass 7977

This theorem is referenced by:  mulrid  8018  mulassi  8030  mulassd  8045  mul12  8150  mul32  8151  mul31  8152  mul4  8153  rimul  8606  divassap  8711  cju  8982  div4p1lem1div2  9239  mulbinom2  10730  sqoddm1div8  10767  remim  11007  imval2  11041  clim2divap  11686  prod3fmul  11687  prodmodclem3  11721  absefib  11917  efieq1re  11918  muldvds1  11962  muldvds2  11963  dvdsmulc  11965  dvdstr  11974  oddprmdvds  12495  cncrng  14068  abssinper  15022  2sqlem6  15277