Theorem mulass 8310

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

Assertion

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

Proof of Theorem mulass

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

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

This proof depends on axioms:  ax-mulass 8282

This theorem is used by:  mulrid  8323  mulassi  8335  mulassd  8349  mul12  8455  mul32  8456  mul31  8457  mul4  8458  rimul  8913  divassap  9020  cju  9291  div4p1lem1div2  9559  mulbinom2  11093  sqoddm1div8  11131  remim  11625  imval2  11659  clim2divap  12307  prod3fmul  12308  prodmodclem3  12342  absefib  12538  efieq1re  12539  muldvds1  12583  muldvds2  12584  dvdsmulc  12586  dvdstr  12595  oddprmdvds  13133  cncrng  14906  abssinper  15947  pellexlem2  16092  2sqlem6  16239