Theorem mulass 8162

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1004   = wceq 1397   ∈ wcel 2202  (class class class)co 6017  ℂcc 8029   · cmul 8036

This theorem was proved from axioms:  ax-mulass 8134

This theorem is referenced by:  mulrid  8175  mulassi  8187  mulassd  8202  mul12  8307  mul32  8308  mul31  8309  mul4  8310  rimul  8764  divassap  8869  cju  9140  div4p1lem1div2  9397  mulbinom2  10917  sqoddm1div8  10954  remim  11420  imval2  11454  clim2divap  12100  prod3fmul  12101  prodmodclem3  12135  absefib  12331  efieq1re  12332  muldvds1  12376  muldvds2  12377  dvdsmulc  12379  dvdstr  12388  oddprmdvds  12926  cncrng  14582  abssinper  15569  2sqlem6  15848