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

Theorem mulassi 10640
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 10613 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4mp3an 1452 1 ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10523   · cmul 10530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 10591
This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1081
This theorem is referenced by:  8th4div3  11845  numma  12130  decbin0  12226  sq4e2t8  13550  3dec  13614  faclbnd4lem1  13641  ef01bndlem  15525  3dvdsdec  15669  3dvds2dec  15670  dec5dvds  16388  karatsuba  16408  sincos4thpi  25026  sincos6thpi  25028  ang180lem2  25315  ang180lem3  25316  asin1  25399  efiatan2  25422  2efiatan  25423  log2cnv  25449  log2ublem2  25452  log2ublem3  25453  log2ub  25454  bclbnd  25783  bposlem8  25794  2lgsoddprmlem3d  25916  ax5seglem7  26648  ipasslem10  28543  siilem1  28555  normlem0  28813  normlem9  28822  bcseqi  28824  polid2i  28861  dfdec100  30473  dpmul100  30500  dpmul1000  30502  dpexpp1  30511  dpmul4  30517  quad3  32810  iexpire  32864  fourierswlem  42392  fouriersw  42393  41prothprm  43661  tgoldbachlt  43858
  Copyright terms: Public domain W3C validator