Theorem mulass 8038

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1372   ∈ wcel 2175  (class class class)co 5934  ℂcc 7905   · cmul 7912

This theorem was proved from axioms:  ax-mulass 8010

This theorem is referenced by:  mulrid  8051  mulassi  8063  mulassd  8078  mul12  8183  mul32  8184  mul31  8185  mul4  8186  rimul  8640  divassap  8745  cju  9016  div4p1lem1div2  9273  mulbinom2  10782  sqoddm1div8  10819  remim  11090  imval2  11124  clim2divap  11770  prod3fmul  11771  prodmodclem3  11805  absefib  12001  efieq1re  12002  muldvds1  12046  muldvds2  12047  dvdsmulc  12049  dvdstr  12058  oddprmdvds  12596  cncrng  14249  abssinper  15236  2sqlem6  15515