Theorem mulass 8126

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1002   = wceq 1395   ∈ wcel 2200  (class class class)co 6000  ℂcc 7993   · cmul 8000

This theorem was proved from axioms:  ax-mulass 8098

This theorem is referenced by:  mulrid  8139  mulassi  8151  mulassd  8166  mul12  8271  mul32  8272  mul31  8273  mul4  8274  rimul  8728  divassap  8833  cju  9104  div4p1lem1div2  9361  mulbinom2  10873  sqoddm1div8  10910  remim  11366  imval2  11400  clim2divap  12046  prod3fmul  12047  prodmodclem3  12081  absefib  12277  efieq1re  12278  muldvds1  12322  muldvds2  12323  dvdsmulc  12325  dvdstr  12334  oddprmdvds  12872  cncrng  14527  abssinper  15514  2sqlem6  15793