MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addassi Unicode version

Theorem addassi 9625
Description: Associative law for addition. (Contributed by NM, 23-Nov-1994.)
Hypotheses
Ref Expression
axi.1
axi.2
axi.3
Assertion
Ref Expression
addassi

Proof of Theorem addassi
StepHypRef Expression
1 axi.1 . 2
2 axi.2 . 2
3 axi.3 . 2
4 addass 9600 . 2
51, 2, 3, 4mp3an 1324 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  e.wcel 1818  (class class class)co 6296   cc 9511   caddc 9516
This theorem is referenced by:  mul02lem2  9778  addid1  9781  2p2e4  10678  3p2e5  10693  3p3e6  10694  4p2e6  10695  4p3e7  10696  4p4e8  10697  5p2e7  10698  5p3e8  10699  5p4e9  10700  5p5e10  10701  6p2e8  10702  6p3e9  10703  6p4e10  10704  7p2e9  10705  7p3e10  10706  8p2e10  10707  numsuc  11016  nummac  11036  numaddc  11039  6p5lem  11053  binom2i  12277  faclbnd4lem1  12371  gcdaddmlem  14166  mod2xnegi  14557  decexp2  14561  decsplit  14569  lgsdir2lem2  23599  ax5seglem7  24238  normlem3  26029  stadd3i  27167  quad3  29024  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  unitadd  38016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 9578
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator