Theorem mulassi 11248

Description: Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)

Hypotheses

Ref	Expression
axi.1	⊢ 𝐴 ∈ ℂ
axi.2	⊢ 𝐵 ∈ ℂ
axi.3	⊢ 𝐶 ∈ ℂ

Assertion

Ref	Expression
mulassi	⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))

Proof of Theorem mulassi

Step	Hyp	Ref	Expression
1		axi.1	. 2 ⊢ 𝐴 ∈ ℂ
2		axi.2	. 2 ⊢ 𝐵 ∈ ℂ
3		axi.3	. 2 ⊢ 𝐶 ∈ ℂ
4		mulass 11216	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	mp3an 1490	1 ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145  (class class class)co 7417  ℂcc 11126   · cmul 11133

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 11194

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  8th4div3  12492  numma  12789  decbin0  12887  sq4e2t8  14267  3dec  14334  faclbnd4lem1  14361  ef01bndlem  16278  3dvdsdec  16428  3dvds2dec  16429  dec5dvds  17162  karatsuba  17181  sincos4thpi  26758  sincos6thpi  26761  ang180lem2  27055  ang180lem3  27056  asin1  27139  efiatan2  27162  2efiatan  27163  log2cnv  27189  log2ublem2  27192  log2ublem3  27193  log2ub  27194  bclbnd  27524  bposlem8  27535  2lgsoddprmlem3d  27657  ax5seglem7  29400  ipasslem10  31328  siilem1  31340  normlem0  31598  normlem9  31607  bcseqi  31609  polid2i  31646  dfdec100  33308  dpmul100  33350  dpmul1000  33352  dpexpp1  33361  dpmul4  33367  quad3  36257  iexpire  36322  mulassnni  42860  sn-1ticom  43318  sn-0tie0  43347  fourierswlem  47066  fouriersw  47067  cos5t  47751  goldpolyfactor  47753  goldratmolem2  47759  goldratmolem3  47760  41prothprm  48530  tgoldbachlt  48740