Theorem mulass 10421

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

Assertion

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

Proof of Theorem mulass

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

Syntax hints:   → wi 4   ∧ w3a 1068   = wceq 1507   ∈ wcel 2050  (class class class)co 6974  ℂcc 10331   · cmul 10338

This theorem was proved from axioms:  ax-mulass 10399

This theorem is referenced by:  mulid1  10435  mulassi  10449  mulassd  10461  mul12  10603  mul32  10604  mul31  10605  mul4  10606  00id  10613  divass  11115  cju  11433  div4p1lem1div2  11700  xmulasslem3  12493  mulbinom2  13397  sqoddm1div8  13417  faclbnd5  13471  bcval5  13491  remim  14335  imval2  14369  sqrlem7  14467  sqrtneglem  14485  sqreulem  14578  clim2div  15103  prodfmul  15104  prodmolem3  15145  sinhval  15365  coshval  15366  absefib  15409  efieq1re  15410  muldvds1  15492  muldvds2  15493  dvdsmulc  15495  dvdsmulcr  15497  dvdstr  15504  eulerthlem2  15973  oddprmdvds  16093  ablfacrp  18950  cncrng  20280  nmoleub2lem3  23434  cnlmod  23459  itg2mulc  24063  abssinper  24821  sinasin  25180  dchrabl  25544  bposlem6  25579  bposlem9  25582  2sqlem6  25713  rpvmasum2  25802  cncvcOLD  28149  ipasslem5  28401  ipasslem11  28406  dvasin  34448  pellexlem2  38852  jm2.25  39021  expgrowth  40112  2zrngmsgrp  43607  nn0sumshdiglemA  44072