Theorem mulassi 11272

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

Syntax hints:   = wceq 1540   ∈ wcel 2108  (class class class)co 7431  ℂcc 11153   · cmul 11160

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

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

This theorem is referenced by:  8th4div3  12486  numma  12777  decbin0  12873  sq4e2t8  14238  3dec  14305  faclbnd4lem1  14332  ef01bndlem  16220  3dvdsdec  16369  3dvds2dec  16370  dec5dvds  17102  karatsuba  17121  sincos4thpi  26555  sincos6thpi  26558  ang180lem2  26853  ang180lem3  26854  asin1  26937  efiatan2  26960  2efiatan  26961  log2cnv  26987  log2ublem2  26990  log2ublem3  26991  log2ub  26992  bclbnd  27324  bposlem8  27335  2lgsoddprmlem3d  27457  ax5seglem7  28950  ipasslem10  30858  siilem1  30870  normlem0  31128  normlem9  31137  bcseqi  31139  polid2i  31176  dfdec100  32832  dpmul100  32879  dpmul1000  32881  dpexpp1  32890  dpmul4  32896  quad3  35675  iexpire  35735  mulassnni  41987  sn-1ticom  42464  sn-0tie0  42469  sn-inelr  42497  fourierswlem  46245  fouriersw  46246  41prothprm  47606  tgoldbachlt  47803