Theorem mulass 8300

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1009   = wceq 1402   ∈ wcel 2209  (class class class)co 6075  ℂcc 8167   · cmul 8174

This theorem was proved from axioms:  ax-mulass 8272

This theorem is referenced by:  mulrid  8313  mulassi  8325  mulassd  8339  mul12  8445  mul32  8446  mul31  8447  mul4  8448  rimul  8903  divassap  9010  cju  9281  div4p1lem1div2  9538  mulbinom2  11071  sqoddm1div8  11109  remim  11603  imval2  11637  clim2divap  12285  prod3fmul  12286  prodmodclem3  12320  absefib  12516  efieq1re  12517  muldvds1  12561  muldvds2  12562  dvdsmulc  12564  dvdstr  12573  oddprmdvds  13111  cncrng  14878  abssinper  15870  pellexlem2  16006  2sqlem6  16153