Theorem mulassi 11133

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

Syntax hints:   = wceq 1541   ∈ wcel 2113  (class class class)co 7355  ℂcc 11014   · cmul 11021

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

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

This theorem is referenced by:  8th4div3  12351  numma  12642  decbin0  12738  sq4e2t8  14116  3dec  14183  faclbnd4lem1  14210  ef01bndlem  16103  3dvdsdec  16253  3dvds2dec  16254  dec5dvds  16986  karatsuba  17005  sincos4thpi  26459  sincos6thpi  26462  ang180lem2  26757  ang180lem3  26758  asin1  26841  efiatan2  26864  2efiatan  26865  log2cnv  26891  log2ublem2  26894  log2ublem3  26895  log2ub  26896  bclbnd  27228  bposlem8  27239  2lgsoddprmlem3d  27361  ax5seglem7  28924  ipasslem10  30830  siilem1  30842  normlem0  31100  normlem9  31109  bcseqi  31111  polid2i  31148  dfdec100  32824  dpmul100  32888  dpmul1000  32890  dpexpp1  32899  dpmul4  32905  quad3  35725  iexpire  35790  mulassnni  42089  sn-1ticom  42543  sn-0tie0  42559  fourierswlem  46342  fouriersw  46343  41prothprm  47733  tgoldbachlt  47930