Theorem mulassi 10917

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

Syntax hints:   = wceq 1539   ∈ wcel 2108  (class class class)co 7255  ℂcc 10800   · cmul 10807

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

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

This theorem is referenced by:  8th4div3  12123  numma  12410  decbin0  12506  sq4e2t8  13844  3dec  13908  faclbnd4lem1  13935  ef01bndlem  15821  3dvdsdec  15969  3dvds2dec  15970  dec5dvds  16693  karatsuba  16713  sincos4thpi  25575  sincos6thpi  25577  ang180lem2  25865  ang180lem3  25866  asin1  25949  efiatan2  25972  2efiatan  25973  log2cnv  25999  log2ublem2  26002  log2ublem3  26003  log2ub  26004  bclbnd  26333  bposlem8  26344  2lgsoddprmlem3d  26466  ax5seglem7  27206  ipasslem10  29102  siilem1  29114  normlem0  29372  normlem9  29381  bcseqi  29383  polid2i  29420  dfdec100  31046  dpmul100  31073  dpmul1000  31075  dpexpp1  31084  dpmul4  31090  quad3  33528  iexpire  33607  mulassnni  39923  sn-1ticom  40337  sn-0tie0  40342  sn-inelr  40356  fourierswlem  43661  fouriersw  43662  41prothprm  44959  tgoldbachlt  45156