Theorem mulassi 11246

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127   · cmul 11134

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

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  8th4div3  12461  numma  12752  decbin0  12848  sq4e2t8  14217  3dec  14284  faclbnd4lem1  14311  ef01bndlem  16202  3dvdsdec  16351  3dvds2dec  16352  dec5dvds  17084  karatsuba  17103  sincos4thpi  26474  sincos6thpi  26477  ang180lem2  26772  ang180lem3  26773  asin1  26856  efiatan2  26879  2efiatan  26880  log2cnv  26906  log2ublem2  26909  log2ublem3  26910  log2ub  26911  bclbnd  27243  bposlem8  27254  2lgsoddprmlem3d  27376  ax5seglem7  28914  ipasslem10  30820  siilem1  30832  normlem0  31090  normlem9  31099  bcseqi  31101  polid2i  31138  dfdec100  32809  dpmul100  32871  dpmul1000  32873  dpexpp1  32882  dpmul4  32888  quad3  35692  iexpire  35752  mulassnni  41999  sn-1ticom  42477  sn-0tie0  42482  sn-inelr  42510  fourierswlem  46259  fouriersw  46260  41prothprm  47633  tgoldbachlt  47830