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

Theorem addassi 10008
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 9983 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4mp3an 1421 1 ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  wcel 1987  (class class class)co 6615  cc 9894   + caddc 9899
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 9961
This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1038
This theorem is referenced by:  mul02lem2  10173  addid1  10176  2p2e4  11104  3p2e5  11120  3p3e6  11121  4p2e6  11122  4p3e7  11123  4p4e8  11124  5p2e7  11125  5p3e8  11126  5p4e9  11127  5p5e10OLD  11128  6p2e8  11129  6p3e9  11130  6p4e10OLD  11131  7p2e9  11132  7p3e10OLD  11133  8p2e10OLD  11134  numsuc  11471  nummac  11518  numaddc  11521  6p5lem  11555  5p5e10  11556  6p4e10  11558  7p3e10  11563  8p2e10  11570  binom2i  12930  faclbnd4lem1  13036  3dvdsdec  14997  3dvdsdecOLD  14998  3dvds2dec  14999  3dvds2decOLD  15000  gcdaddmlem  15188  mod2xnegi  15718  decexp2  15722  decsplit  15730  decsplitOLD  15734  lgsdir2lem2  24985  2lgsoddprmlem3d  25072  ax5seglem7  25749  normlem3  27857  stadd3i  28995  quad3  31325  unitadd  38019  sqwvfoura  39782  sqwvfourb  39783  fouriersw  39785  3exp4mod41  40862  bgoldbtbndlem1  41012
  Copyright terms: Public domain W3C validator