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

Theorem mulassi 9993
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 9968 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4mp3an 1421 1 ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wcel 1987  (class class class)co 6604  cc 9878   · cmul 9885
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 9946
This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038
This theorem is referenced by:  8th4div3  11196  numma  11501  decbin0  11626  sq4e2t8  12902  3dec  12990  3decOLD  12993  faclbnd4lem1  13020  ef01bndlem  14839  3dvdsdec  14978  3dvdsdecOLD  14979  3dvds2dec  14980  3dvds2decOLD  14981  dec5dvds  15692  karatsuba  15716  karatsubaOLD  15717  sincos4thpi  24169  sincos6thpi  24171  ang180lem2  24440  ang180lem3  24441  asin1  24521  efiatan2  24544  2efiatan  24545  log2cnv  24571  log2ublem2  24574  log2ublem3  24575  log2ub  24576  bclbnd  24905  bposlem8  24916  2lgsoddprmlem3d  25038  ax5seglem7  25715  ipasslem10  27540  siilem1  27552  normlem0  27812  normlem9  27821  bcseqi  27823  polid2i  27860  quad3  31269  iexpire  31326  fourierswlem  39751  fouriersw  39752  41prothprm  40832  tgoldbachlt  40988  tgoldbachltOLD  40995
  Copyright terms: Public domain W3C validator