Theorem mulass 7959

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 979   = wceq 1363   ∈ wcel 2159  (class class class)co 5890  ℂcc 7826   · cmul 7833

This theorem was proved from axioms:  ax-mulass 7931

This theorem is referenced by:  mulrid  7971  mulassi  7983  mulassd  7998  mul12  8103  mul32  8104  mul31  8105  mul4  8106  rimul  8559  divassap  8664  cju  8935  div4p1lem1div2  9189  mulbinom2  10654  sqoddm1div8  10691  remim  10886  imval2  10920  clim2divap  11565  prod3fmul  11566  prodmodclem3  11600  absefib  11795  efieq1re  11796  muldvds1  11840  muldvds2  11841  dvdsmulc  11843  dvdstr  11852  oddprmdvds  12369  cncrng  13832  abssinper  14650  2sqlem6  14850