Theorem mulassi 10375

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

Syntax hints:   = wceq 1656   ∈ wcel 2164  (class class class)co 6910  ℂcc 10257   · cmul 10264

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

This theorem depends on definitions:  df-bi 199  df-an 387  df-3an 1113

This theorem is referenced by:  8th4div3  11585  numma  11873  decbin0  11970  sq4e2t8  13263  3dec  13353  faclbnd4lem1  13380  ef01bndlem  15293  3dvdsdec  15437  3dvds2dec  15438  dec5dvds  16146  karatsuba  16166  sincos4thpi  24672  sincos6thpi  24674  ang180lem2  24957  ang180lem3  24958  asin1  25041  efiatan2  25064  2efiatan  25065  log2cnv  25091  log2ublem2  25094  log2ublem3  25095  log2ub  25096  bclbnd  25425  bposlem8  25436  2lgsoddprmlem3d  25558  ax5seglem7  26241  ipasslem10  28245  siilem1  28257  normlem0  28517  normlem9  28526  bcseqi  28528  polid2i  28565  dfdec100  30119  dpmul100  30146  dpmul1000  30148  dpexpp1  30157  dpmul4  30163  quad3  32104  iexpire  32159  fourierswlem  41235  fouriersw  41236  41prothprm  42380  tgoldbachlt  42548