Theorem mulass 7846

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 963   = wceq 1335   ∈ wcel 2128  (class class class)co 5818  ℂcc 7713   · cmul 7720

This theorem was proved from axioms:  ax-mulass 7818

This theorem is referenced by:  mulid1  7858  mulassi  7870  mulassd  7884  mul12  7987  mul32  7988  mul31  7989  mul4  7990  rimul  8443  divassap  8546  cju  8815  div4p1lem1div2  9069  mulbinom2  10516  sqoddm1div8  10553  remim  10742  imval2  10776  clim2divap  11419  prod3fmul  11420  prodmodclem3  11454  absefib  11649  efieq1re  11650  muldvds1  11693  muldvds2  11694  dvdsmulc  11696  dvdstr  11705  abssinper  13127