Theorem mulass 8003

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2164  (class class class)co 5918  ℂcc 7870   · cmul 7877

This theorem was proved from axioms:  ax-mulass 7975

This theorem is referenced by:  mulrid  8016  mulassi  8028  mulassd  8043  mul12  8148  mul32  8149  mul31  8150  mul4  8151  rimul  8604  divassap  8709  cju  8980  div4p1lem1div2  9236  mulbinom2  10727  sqoddm1div8  10764  remim  11004  imval2  11038  clim2divap  11683  prod3fmul  11684  prodmodclem3  11718  absefib  11914  efieq1re  11915  muldvds1  11959  muldvds2  11960  dvdsmulc  11962  dvdstr  11971  oddprmdvds  12492  cncrng  14057  abssinper  14981  2sqlem6  15207