Theorem mulass 7944

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 978   = wceq 1353   ∈ wcel 2148  (class class class)co 5877  ℂcc 7811   · cmul 7818

This theorem was proved from axioms:  ax-mulass 7916

This theorem is referenced by:  mulrid  7956  mulassi  7968  mulassd  7983  mul12  8088  mul32  8089  mul31  8090  mul4  8091  rimul  8544  divassap  8649  cju  8920  div4p1lem1div2  9174  mulbinom2  10639  sqoddm1div8  10676  remim  10871  imval2  10905  clim2divap  11550  prod3fmul  11551  prodmodclem3  11585  absefib  11780  efieq1re  11781  muldvds1  11825  muldvds2  11826  dvdsmulc  11828  dvdstr  11837  oddprmdvds  12354  cncrng  13502  abssinper  14306  2sqlem6  14506