Theorem mulassi 9928

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

Syntax hints:   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   · cmul 9820

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

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  8th4div3  11129  numma  11433  decbin0  11558  sq4e2t8  12824  3dec  12912  3decOLD  12915  faclbnd4lem1  12942  ef01bndlem  14753  3dvdsdec  14892  3dvdsdecOLD  14893  3dvds2dec  14894  3dvds2decOLD  14895  dec5dvds  15606  karatsuba  15630  karatsubaOLD  15631  sincos4thpi  24069  sincos6thpi  24071  ang180lem2  24340  ang180lem3  24341  asin1  24421  efiatan2  24444  2efiatan  24445  log2cnv  24471  log2ublem2  24474  log2ublem3  24475  log2ub  24476  bclbnd  24805  bposlem8  24816  2lgsoddprmlem3d  24938  ax5seglem7  25615  ipasslem10  27078  siilem1  27090  normlem0  27350  normlem9  27359  bcseqi  27361  polid2i  27398  quad3  30818  iexpire  30874  fourierswlem  39123  fouriersw  39124  41prothprm  40074  tgoldbachlt  40230  tgoldbachltOLD  40237