Theorem mulass 8206

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1005   = wceq 1398   ∈ wcel 2202  (class class class)co 6028  ℂcc 8073   · cmul 8080

This theorem was proved from axioms:  ax-mulass 8178

This theorem is referenced by:  mulrid  8219  mulassi  8231  mulassd  8245  mul12  8350  mul32  8351  mul31  8352  mul4  8353  rimul  8807  divassap  8912  cju  9183  div4p1lem1div2  9440  mulbinom2  10964  sqoddm1div8  11001  remim  11483  imval2  11517  clim2divap  12164  prod3fmul  12165  prodmodclem3  12199  absefib  12395  efieq1re  12396  muldvds1  12440  muldvds2  12441  dvdsmulc  12443  dvdstr  12452  oddprmdvds  12990  cncrng  14648  abssinper  15640  pellexlem2  15775  2sqlem6  15922