Theorem mulassi 11255

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  (class class class)co 7417  ℂcc 11136   · cmul 11143

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

This theorem depends on definitions:  df-bi 206  df-an 395  df-3an 1086

This theorem is referenced by:  8th4div3  12462  numma  12751  decbin0  12847  sq4e2t8  14194  3dec  14257  faclbnd4lem1  14284  ef01bndlem  16160  3dvdsdec  16308  3dvds2dec  16309  dec5dvds  17032  karatsuba  17052  sincos4thpi  26478  sincos6thpi  26480  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  28802  ipasslem10  30705  siilem1  30717  normlem0  30975  normlem9  30984  bcseqi  30986  polid2i  31023  dfdec100  32650  dpmul100  32677  dpmul1000  32679  dpexpp1  32688  dpmul4  32694  quad3  35344  iexpire  35399  mulassnni  41526  sn-1ticom  42054  sn-0tie0  42059  sn-inelr  42085  fourierswlem  45681  fouriersw  45682  41prothprm  47022  tgoldbachlt  47219