Theorem mulassi 11221

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

Syntax hints:   = wceq 1533   ∈ wcel 2098  (class class class)co 7401  ℂcc 11103   · cmul 11110

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

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

This theorem is referenced by:  8th4div3  12428  numma  12717  decbin0  12813  sq4e2t8  14159  3dec  14222  faclbnd4lem1  14249  ef01bndlem  16123  3dvdsdec  16271  3dvds2dec  16272  dec5dvds  16993  karatsuba  17013  sincos4thpi  26353  sincos6thpi  26355  ang180lem2  26646  ang180lem3  26647  asin1  26730  efiatan2  26753  2efiatan  26754  log2cnv  26780  log2ublem2  26783  log2ublem3  26784  log2ub  26785  bclbnd  27117  bposlem8  27128  2lgsoddprmlem3d  27250  ax5seglem7  28617  ipasslem10  30516  siilem1  30528  normlem0  30786  normlem9  30795  bcseqi  30797  polid2i  30834  dfdec100  32460  dpmul100  32487  dpmul1000  32489  dpexpp1  32498  dpmul4  32504  quad3  35110  iexpire  35166  mulassnni  41311  sn-1ticom  41762  sn-0tie0  41767  sn-inelr  41793  fourierswlem  45397  fouriersw  45398  41prothprm  46738  tgoldbachlt  46935