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

Theorem mulassi 10650
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 10623 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
51, 2, 3, 4mp3an 1458 1 ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2115  (class class class)co 7149  cc 10533   · cmul 10540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-mulass 10601
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086
This theorem is referenced by:  8th4div3  11854  numma  12139  decbin0  12235  sq4e2t8  13567  3dec  13631  faclbnd4lem1  13658  ef01bndlem  15537  3dvdsdec  15681  3dvds2dec  15682  dec5dvds  16398  karatsuba  16418  sincos4thpi  25113  sincos6thpi  25115  ang180lem2  25403  ang180lem3  25404  asin1  25487  efiatan2  25510  2efiatan  25511  log2cnv  25537  log2ublem2  25540  log2ublem3  25541  log2ub  25542  bclbnd  25871  bposlem8  25882  2lgsoddprmlem3d  26004  ax5seglem7  26736  ipasslem10  28629  siilem1  28641  normlem0  28899  normlem9  28908  bcseqi  28910  polid2i  28947  dfdec100  30561  dpmul100  30588  dpmul1000  30590  dpexpp1  30599  dpmul4  30605  quad3  32974  iexpire  33028  mulassnni  39226  3lexlogpow5ineq1  39293  sn-1ticom  39505  sn-inelr  39515  fourierswlem  42803  fouriersw  42804  41prothprm  44068  tgoldbachlt  44265
  Copyright terms: Public domain W3C validator