Theorem mulass 8012

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2167  (class class class)co 5923  ℂcc 7879   · cmul 7886

This theorem was proved from axioms:  ax-mulass 7984

This theorem is referenced by:  mulrid  8025  mulassi  8037  mulassd  8052  mul12  8157  mul32  8158  mul31  8159  mul4  8160  rimul  8614  divassap  8719  cju  8990  div4p1lem1div2  9247  mulbinom2  10750  sqoddm1div8  10787  remim  11027  imval2  11061  clim2divap  11707  prod3fmul  11708  prodmodclem3  11742  absefib  11938  efieq1re  11939  muldvds1  11983  muldvds2  11984  dvdsmulc  11986  dvdstr  11995  oddprmdvds  12533  cncrng  14135  abssinper  15092  2sqlem6  15371