Theorem mulass 8311

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

Assertion

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

Proof of Theorem mulass

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

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

This proof depends on axioms:  ax-mulass 8283

This theorem is used by:  mulrid  8324  mulassi  8336  mulassd  8350  mul12  8457  mul32  8458  mul31  8459  mul4  8460  rimul  8916  divassap  9023  cju  9294  div4p1lem1div2  9564  mulbinom2  11108  sqoddm1div8  11146  remim  11641  imval2  11675  clim2divap  12326  prod3fmul  12327  prodmodclem3  12361  absefib  12557  efieq1re  12558  muldvds1  12602  muldvds2  12603  dvdsmulc  12605  dvdstr  12614  oddprmdvds  13156  cncrng  14990  abssinper  16039  pellexlem2  16191  bposlem6  16277  bposlem9  16280  2sqlem6  16405