Theorem mulass 7941

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 978   = wceq 1353   ∈ wcel 2148  (class class class)co 5874  ℂcc 7808   · cmul 7815

This theorem was proved from axioms:  ax-mulass 7913

This theorem is referenced by:  mulrid  7953  mulassi  7965  mulassd  7980  mul12  8085  mul32  8086  mul31  8087  mul4  8088  rimul  8541  divassap  8646  cju  8917  div4p1lem1div2  9171  mulbinom2  10636  sqoddm1div8  10673  remim  10868  imval2  10902  clim2divap  11547  prod3fmul  11548  prodmodclem3  11582  absefib  11777  efieq1re  11778  muldvds1  11822  muldvds2  11823  dvdsmulc  11825  dvdstr  11834  oddprmdvds  12351  cncrng  13433  abssinper  14237  2sqlem6  14437