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

Theorem mulassi 10239
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 10214 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4mp3an 1571 1 ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1630  wcel 2137  (class class class)co 6811  cc 10124   · cmul 10131
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 10192
This theorem depends on definitions:  df-bi 197  df-an 385  df-3an 1074
This theorem is referenced by:  8th4div3  11442  numma  11747  decbin0  11872  sq4e2t8  13154  3dec  13242  3decOLD  13245  faclbnd4lem1  13272  ef01bndlem  15111  3dvdsdec  15254  3dvdsdecOLD  15255  3dvds2dec  15256  3dvds2decOLD  15257  dec5dvds  15968  karatsuba  15992  karatsubaOLD  15993  sincos4thpi  24462  sincos6thpi  24464  ang180lem2  24737  ang180lem3  24738  asin1  24818  efiatan2  24841  2efiatan  24842  log2cnv  24868  log2ublem2  24871  log2ublem3  24872  log2ub  24873  bclbnd  25202  bposlem8  25213  2lgsoddprmlem3d  25335  ax5seglem7  26012  ipasslem10  28001  siilem1  28013  normlem0  28273  normlem9  28282  bcseqi  28284  polid2i  28321  dfdec100  29883  dpmul100  29912  dpmul1000  29914  dpexpp1  29923  dpmul4  29929  quad3  31869  iexpire  31926  fourierswlem  40948  fouriersw  40949  41prothprm  42044  tgoldbachlt  42212  tgoldbachltOLD  42218
  Copyright terms: Public domain W3C validator