Theorem mulass 8029

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   · cmul 7903

This theorem was proved from axioms:  ax-mulass 8001

This theorem is referenced by:  mulrid  8042  mulassi  8054  mulassd  8069  mul12  8174  mul32  8175  mul31  8176  mul4  8177  rimul  8631  divassap  8736  cju  9007  div4p1lem1div2  9264  mulbinom2  10767  sqoddm1div8  10804  remim  11044  imval2  11078  clim2divap  11724  prod3fmul  11725  prodmodclem3  11759  absefib  11955  efieq1re  11956  muldvds1  12000  muldvds2  12001  dvdsmulc  12003  dvdstr  12012  oddprmdvds  12550  cncrng  14203  abssinper  15190  2sqlem6  15469