Theorem mulassi 11347

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  (class class class)co 7443  ℂcc 11225   · cmul 11232

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 11293

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  8th4div3  12593  numma  12890  decbin0  12988  sq4e2t8  14369  3dec  14437  faclbnd4lem1  14464  ef01bndlem  16381  3dvdsdec  16531  3dvds2dec  16532  dec5dvds  17271  karatsuba  17290  sincos4thpi  26872  sincos6thpi  26874  ang180lem2  27168  ang180lem3  27169  asin1  27252  efiatan2  27275  2efiatan  27276  log2cnv  27302  log2ublem2  27305  log2ublem3  27306  log2ub  27307  bclbnd  27637  bposlem8  27648  2lgsoddprmlem3d  27770  ax5seglem7  29543  ipasslem10  31471  siilem1  31483  normlem0  31741  normlem9  31750  bcseqi  31752  polid2i  31789  dfdec100  33491  dpmul100  33533  dpmul1000  33535  dpexpp1  33544  dpmul4  33550  quad3  36602  iexpire  36678  mulassnni  43228  sn-1ticom  43679  sn-0tie0  43708  fourierswlem  47445  fouriersw  47446  cos5t  48130  goldpolyfactor  48132  goldratmolem2  48138  goldratmolem3  48139  41prothprm  48909  tgoldbachlt  49119