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  11114  sqoddm1div8  11152  remim  11647  imval2  11681  clim2divap  12332  prod3fmul  12333  prodmodclem3  12367  absefib  12563  efieq1re  12564  muldvds1  12608  muldvds2  12609  dvdsmulc  12611  dvdstr  12620  oddprmdvds  13162  cncrng  15015  abssinper  16073  pellexlem2  16230  bposlem6  16316  bposlem9  16319  2sqlem6  16444