Theorem mulassi 11154

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 11124	. 2 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
5	1, 2, 3, 4	mp3an 1469	1 ⊢ ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))

Syntax hints:   = wceq 1547   ∈ wcel 2119  (class class class)co 7363  ℂcc 11034   · cmul 11041

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 11102

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094

This theorem is referenced by:  8th4div3  12395  numma  12686  decbin0  12782  sq4e2t8  14159  3dec  14226  faclbnd4lem1  14253  ef01bndlem  16149  3dvdsdec  16299  3dvds2dec  16300  dec5dvds  17033  karatsuba  17052  sincos4thpi  26502  sincos6thpi  26505  ang180lem2  26799  ang180lem3  26800  asin1  26883  efiatan2  26906  2efiatan  26907  log2cnv  26933  log2ublem2  26936  log2ublem3  26937  log2ub  26938  bclbnd  27268  bposlem8  27279  2lgsoddprmlem3d  27401  ax5seglem7  29029  ipasslem10  30935  siilem1  30947  normlem0  31205  normlem9  31214  bcseqi  31216  polid2i  31253  dfdec100  32929  dpmul100  32982  dpmul1000  32984  dpexpp1  32993  dpmul4  32999  quad3  35905  iexpire  35970  mulassnni  42478  sn-1ticom  42919  sn-0tie0  42948  fourierswlem  46680  fouriersw  46681  cos5t  47349  goldratmolem2  47356  41prothprm  48104  tgoldbachlt  48314