Theorem mulass 8274

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1005   = wceq 1398   ∈ wcel 2205  (class class class)co 6058  ℂcc 8141   · cmul 8148

This theorem was proved from axioms:  ax-mulass 8246

This theorem is referenced by:  mulrid  8287  mulassi  8299  mulassd  8313  mul12  8419  mul32  8420  mul31  8421  mul4  8422  rimul  8877  divassap  8984  cju  9255  div4p1lem1div2  9512  mulbinom2  11045  sqoddm1div8  11083  remim  11573  imval2  11607  clim2divap  12254  prod3fmul  12255  prodmodclem3  12289  absefib  12485  efieq1re  12486  muldvds1  12530  muldvds2  12531  dvdsmulc  12533  dvdstr  12542  oddprmdvds  13080  cncrng  14846  abssinper  15840  pellexlem2  15975  2sqlem6  16122