Theorem mulassi 11087

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

Syntax hints:   = wceq 1540   ∈ wcel 2105  (class class class)co 7337  ℂcc 10970   · cmul 10977

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

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088

This theorem is referenced by:  8th4div3  12294  numma  12582  decbin0  12678  sq4e2t8  14017  3dec  14081  faclbnd4lem1  14108  ef01bndlem  15992  3dvdsdec  16140  3dvds2dec  16141  dec5dvds  16862  karatsuba  16882  sincos4thpi  25776  sincos6thpi  25778  ang180lem2  26066  ang180lem3  26067  asin1  26150  efiatan2  26173  2efiatan  26174  log2cnv  26200  log2ublem2  26203  log2ublem3  26204  log2ub  26205  bclbnd  26534  bposlem8  26545  2lgsoddprmlem3d  26667  ax5seglem7  27592  ipasslem10  29489  siilem1  29501  normlem0  29759  normlem9  29768  bcseqi  29770  polid2i  29807  dfdec100  31431  dpmul100  31458  dpmul1000  31460  dpexpp1  31469  dpmul4  31475  quad3  33927  iexpire  33991  mulassnni  40257  sn-1ticom  40684  sn-0tie0  40689  sn-inelr  40703  fourierswlem  44116  fouriersw  44117  41prothprm  45431  tgoldbachlt  45628