MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mulassi Structured version   Visualization version   GIF version

Theorem mulassi 11272
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
StepHypRef Expression
1 axi.1 . 2 𝐴 ∈ ℂ
2 axi.2 . 2 𝐵 ∈ ℂ
3 axi.3 . 2 𝐶 ∈ ℂ
4 mulass 11243 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4mp3an 1463 1 ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wcel 2108  (class class class)co 7431  cc 11153   · cmul 11160
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 11221
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089
This theorem is referenced by:  8th4div3  12486  numma  12777  decbin0  12873  sq4e2t8  14238  3dec  14305  faclbnd4lem1  14332  ef01bndlem  16220  3dvdsdec  16369  3dvds2dec  16370  dec5dvds  17102  karatsuba  17121  sincos4thpi  26555  sincos6thpi  26558  ang180lem2  26853  ang180lem3  26854  asin1  26937  efiatan2  26960  2efiatan  26961  log2cnv  26987  log2ublem2  26990  log2ublem3  26991  log2ub  26992  bclbnd  27324  bposlem8  27335  2lgsoddprmlem3d  27457  ax5seglem7  28950  ipasslem10  30858  siilem1  30870  normlem0  31128  normlem9  31137  bcseqi  31139  polid2i  31176  dfdec100  32832  dpmul100  32879  dpmul1000  32881  dpexpp1  32890  dpmul4  32896  quad3  35675  iexpire  35735  mulassnni  41987  sn-1ticom  42464  sn-0tie0  42469  sn-inelr  42497  fourierswlem  46245  fouriersw  46246  41prothprm  47606  tgoldbachlt  47803
  Copyright terms: Public domain W3C validator