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

Theorem mulassi 9928
 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 9903 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4mp3an 1416 1 ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   · cmul 9820 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 9881 This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033 This theorem is referenced by:  8th4div3  11129  numma  11433  decbin0  11558  sq4e2t8  12824  3dec  12912  3decOLD  12915  faclbnd4lem1  12942  ef01bndlem  14753  3dvdsdec  14892  3dvdsdecOLD  14893  3dvds2dec  14894  3dvds2decOLD  14895  dec5dvds  15606  karatsuba  15630  karatsubaOLD  15631  sincos4thpi  24069  sincos6thpi  24071  ang180lem2  24340  ang180lem3  24341  asin1  24421  efiatan2  24444  2efiatan  24445  log2cnv  24471  log2ublem2  24474  log2ublem3  24475  log2ub  24476  bclbnd  24805  bposlem8  24816  2lgsoddprmlem3d  24938  ax5seglem7  25615  ipasslem10  27078  siilem1  27090  normlem0  27350  normlem9  27359  bcseqi  27361  polid2i  27398  quad3  30818  iexpire  30874  fourierswlem  39123  fouriersw  39124  41prothprm  40074  tgoldbachlt  40230  tgoldbachltOLD  40237
 Copyright terms: Public domain W3C validator