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