Theorem mulass 8163

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1004   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   · cmul 8037

This theorem was proved from axioms:  ax-mulass 8135

This theorem is referenced by:  mulrid  8176  mulassi  8188  mulassd  8203  mul12  8308  mul32  8309  mul31  8310  mul4  8311  rimul  8765  divassap  8870  cju  9141  div4p1lem1div2  9398  mulbinom2  10919  sqoddm1div8  10956  remim  11425  imval2  11459  clim2divap  12106  prod3fmul  12107  prodmodclem3  12141  absefib  12337  efieq1re  12338  muldvds1  12382  muldvds2  12383  dvdsmulc  12385  dvdstr  12394  oddprmdvds  12932  cncrng  14589  abssinper  15576  2sqlem6  15855