Theorem mulass 8258

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1005   = wceq 1398   ∈ wcel 2203  (class class class)co 6050  ℂcc 8125   · cmul 8132

This theorem was proved from axioms:  ax-mulass 8230

This theorem is referenced by:  mulrid  8271  mulassi  8283  mulassd  8297  mul12  8402  mul32  8403  mul31  8404  mul4  8405  rimul  8859  divassap  8964  cju  9235  div4p1lem1div2  9492  mulbinom2  11018  sqoddm1div8  11055  remim  11545  imval2  11579  clim2divap  12226  prod3fmul  12227  prodmodclem3  12261  absefib  12457  efieq1re  12458  muldvds1  12502  muldvds2  12503  dvdsmulc  12505  dvdstr  12514  oddprmdvds  13052  cncrng  14717  abssinper  15711  pellexlem2  15846  2sqlem6  15993