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

Theorem mulassi 10375
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 10347 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4mp3an 1589 1 ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1656  wcel 2164  (class class class)co 6910  cc 10257   · cmul 10264
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 10325
This theorem depends on definitions:  df-bi 199  df-an 387  df-3an 1113
This theorem is referenced by:  8th4div3  11585  numma  11873  decbin0  11970  sq4e2t8  13263  3dec  13353  faclbnd4lem1  13380  ef01bndlem  15293  3dvdsdec  15437  3dvds2dec  15438  dec5dvds  16146  karatsuba  16166  sincos4thpi  24672  sincos6thpi  24674  ang180lem2  24957  ang180lem3  24958  asin1  25041  efiatan2  25064  2efiatan  25065  log2cnv  25091  log2ublem2  25094  log2ublem3  25095  log2ub  25096  bclbnd  25425  bposlem8  25436  2lgsoddprmlem3d  25558  ax5seglem7  26241  ipasslem10  28245  siilem1  28257  normlem0  28517  normlem9  28526  bcseqi  28528  polid2i  28565  dfdec100  30119  dpmul100  30146  dpmul1000  30148  dpexpp1  30157  dpmul4  30163  quad3  32104  iexpire  32159  fourierswlem  41235  fouriersw  41236  41prothprm  42380  tgoldbachlt  42548
  Copyright terms: Public domain W3C validator