Theorem mulassi 11247

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

Syntax hints:   = wceq 1534   ∈ wcel 2099  (class class class)co 7414  ℂcc 11128   · cmul 11135

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

This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087

This theorem is referenced by:  8th4div3  12454  numma  12743  decbin0  12839  sq4e2t8  14186  3dec  14249  faclbnd4lem1  14276  ef01bndlem  16152  3dvdsdec  16300  3dvds2dec  16301  dec5dvds  17024  karatsuba  17044  sincos4thpi  26435  sincos6thpi  26437  ang180lem2  26729  ang180lem3  26730  asin1  26813  efiatan2  26836  2efiatan  26837  log2cnv  26863  log2ublem2  26866  log2ublem3  26867  log2ub  26868  bclbnd  27200  bposlem8  27211  2lgsoddprmlem3d  27333  ax5seglem7  28733  ipasslem10  30636  siilem1  30648  normlem0  30906  normlem9  30915  bcseqi  30917  polid2i  30954  dfdec100  32575  dpmul100  32602  dpmul1000  32604  dpexpp1  32613  dpmul4  32619  quad3  35210  iexpire  35265  mulassnni  41394  sn-1ticom  41911  sn-0tie0  41916  sn-inelr  41942  fourierswlem  45541  fouriersw  45542  41prothprm  46882  tgoldbachlt  47079