Theorem mulass 8010

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2167  (class class class)co 5922  ℂcc 7877   · cmul 7884

This theorem was proved from axioms:  ax-mulass 7982

This theorem is referenced by:  mulrid  8023  mulassi  8035  mulassd  8050  mul12  8155  mul32  8156  mul31  8157  mul4  8158  rimul  8612  divassap  8717  cju  8988  div4p1lem1div2  9245  mulbinom2  10748  sqoddm1div8  10785  remim  11025  imval2  11059  clim2divap  11705  prod3fmul  11706  prodmodclem3  11740  absefib  11936  efieq1re  11937  muldvds1  11981  muldvds2  11982  dvdsmulc  11984  dvdstr  11993  oddprmdvds  12523  cncrng  14125  abssinper  15082  2sqlem6  15361