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

Theorem addassi 10249
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 10224 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4mp3an 1571 1 ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1630  wcel 2144  (class class class)co 6792  cc 10135   + caddc 10140
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 10202
This theorem depends on definitions:  df-bi 197  df-an 383  df-3an 1072
This theorem is referenced by:  mul02lem2  10414  addid1  10417  2p2e4  11345  3p2e5  11361  3p3e6  11362  4p2e6  11363  4p3e7  11364  4p4e8  11365  5p2e7  11366  5p3e8  11367  5p4e9  11368  5p5e10OLD  11369  6p2e8  11370  6p3e9  11371  6p4e10OLD  11372  7p2e9  11373  7p3e10OLD  11374  8p2e10OLD  11375  numsuc  11712  nummac  11758  numaddc  11761  6p5lem  11795  5p5e10  11796  6p4e10  11798  7p3e10  11803  8p2e10  11810  binom2i  13180  faclbnd4lem1  13283  3dvdsdec  15262  3dvdsdecOLD  15263  3dvds2dec  15264  gcdaddmlem  15452  mod2xnegi  15981  decexp2  15985  decsplit  15993  decsplitOLD  15997  lgsdir2lem2  25271  2lgsoddprmlem3d  25358  ax5seglem7  26035  normlem3  28303  stadd3i  29441  dfdec100  29910  dp3mul10  29940  dpmul  29955  dpmul4  29956  quad3  31896  unitadd  39017  sqwvfoura  40956  sqwvfourb  40957  fouriersw  40959  3exp4mod41  42051  bgoldbtbndlem1  42211
  Copyright terms: Public domain W3C validator