Theorem mulass 8141

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1002   = wceq 1395   ∈ wcel 2200  (class class class)co 6007  ℂcc 8008   · cmul 8015

This theorem was proved from axioms:  ax-mulass 8113

This theorem is referenced by:  mulrid  8154  mulassi  8166  mulassd  8181  mul12  8286  mul32  8287  mul31  8288  mul4  8289  rimul  8743  divassap  8848  cju  9119  div4p1lem1div2  9376  mulbinom2  10890  sqoddm1div8  10927  remim  11386  imval2  11420  clim2divap  12066  prod3fmul  12067  prodmodclem3  12101  absefib  12297  efieq1re  12298  muldvds1  12342  muldvds2  12343  dvdsmulc  12345  dvdstr  12354  oddprmdvds  12892  cncrng  14548  abssinper  15535  2sqlem6  15814