Theorem mulass 8316

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

Assertion

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

Proof of Theorem mulass

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009   = wceq 1402   ∈ wcel 2209  (class class class)co 6088  ℂcc 8183   · cmul 8190

This proof depends on axioms:  ax-mulass 8288

This theorem is used by:  mulrid  8329  mulassi  8341  mulassd  8355  mul12  8462  mul32  8463  mul31  8464  mul4  8465  rimul  8921  divassap  9028  cju  9299  div4p1lem1div2  9570  mulbinom2  11113  sqoddm1div8  11151  remim  11646  imval2  11680  clim2divap  12331  prod3fmul  12332  prodmodclem3  12366  absefib  12562  efieq1re  12563  muldvds1  12607  muldvds2  12608  dvdsmulc  12610  dvdstr  12619  oddprmdvds  13161  cncrng  15014  abssinper  16090  pellexlem2  16247  bposlem6  16333  bposlem9  16336  2sqlem6  16461