Theorem mulassi 11130

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7352  ℂcc 11011   · cmul 11018

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

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

This theorem is referenced by:  8th4div3  12348  numma  12638  decbin0  12734  sq4e2t8  14108  3dec  14175  faclbnd4lem1  14202  ef01bndlem  16095  3dvdsdec  16245  3dvds2dec  16246  dec5dvds  16978  karatsuba  16997  sincos4thpi  26450  sincos6thpi  26453  ang180lem2  26748  ang180lem3  26749  asin1  26832  efiatan2  26855  2efiatan  26856  log2cnv  26882  log2ublem2  26885  log2ublem3  26886  log2ub  26887  bclbnd  27219  bposlem8  27230  2lgsoddprmlem3d  27352  ax5seglem7  28915  ipasslem10  30821  siilem1  30833  normlem0  31091  normlem9  31100  bcseqi  31102  polid2i  31139  dfdec100  32818  dpmul100  32884  dpmul1000  32886  dpexpp1  32895  dpmul4  32901  quad3  35735  iexpire  35800  mulassnni  42099  sn-1ticom  42553  sn-0tie0  42569  fourierswlem  46352  fouriersw  46353  41prothprm  47743  tgoldbachlt  47940