Theorem mulass 7937

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

Assertion

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

Proof of Theorem mulass

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

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

This theorem was proved from axioms:  ax-mulass 7909

This theorem is referenced by:  mulrid  7949  mulassi  7961  mulassd  7975  mul12  8080  mul32  8081  mul31  8082  mul4  8083  rimul  8536  divassap  8641  cju  8912  div4p1lem1div2  9166  mulbinom2  10629  sqoddm1div8  10666  remim  10860  imval2  10894  clim2divap  11539  prod3fmul  11540  prodmodclem3  11574  absefib  11769  efieq1re  11770  muldvds1  11814  muldvds2  11815  dvdsmulc  11817  dvdstr  11826  oddprmdvds  12342  cncrng  13268  abssinper  14049  2sqlem6  14238