Theorem mulass 8076

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 981   = wceq 1373   ∈ wcel 2177  (class class class)co 5957  ℂcc 7943   · cmul 7950

This theorem was proved from axioms:  ax-mulass 8048

This theorem is referenced by:  mulrid  8089  mulassi  8101  mulassd  8116  mul12  8221  mul32  8222  mul31  8223  mul4  8224  rimul  8678  divassap  8783  cju  9054  div4p1lem1div2  9311  mulbinom2  10823  sqoddm1div8  10860  remim  11246  imval2  11280  clim2divap  11926  prod3fmul  11927  prodmodclem3  11961  absefib  12157  efieq1re  12158  muldvds1  12202  muldvds2  12203  dvdsmulc  12205  dvdstr  12214  oddprmdvds  12752  cncrng  14406  abssinper  15393  2sqlem6  15672