Theorem mulassi 11269

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

Syntax hints:   = wceq 1536   ∈ wcel 2105  (class class class)co 7430  ℂcc 11150   · cmul 11157

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

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

This theorem is referenced by:  8th4div3  12483  numma  12774  decbin0  12870  sq4e2t8  14234  3dec  14301  faclbnd4lem1  14328  ef01bndlem  16216  3dvdsdec  16365  3dvds2dec  16366  dec5dvds  17097  karatsuba  17117  sincos4thpi  26569  sincos6thpi  26572  ang180lem2  26867  ang180lem3  26868  asin1  26951  efiatan2  26974  2efiatan  26975  log2cnv  27001  log2ublem2  27004  log2ublem3  27005  log2ub  27006  bclbnd  27338  bposlem8  27349  2lgsoddprmlem3d  27471  ax5seglem7  28964  ipasslem10  30867  siilem1  30879  normlem0  31137  normlem9  31146  bcseqi  31148  polid2i  31185  dfdec100  32836  dpmul100  32863  dpmul1000  32865  dpexpp1  32874  dpmul4  32880  quad3  35654  iexpire  35714  mulassnni  41967  sn-1ticom  42440  sn-0tie0  42445  sn-inelr  42473  fourierswlem  46185  fouriersw  46186  41prothprm  47543  tgoldbachlt  47740