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

Theorem addassi 11229
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 11200 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4mp3an 1460 1 ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wcel 2105  (class class class)co 7412  cc 11111   + caddc 11116
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 11178
This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1088
This theorem is referenced by:  mul02lem2  11396  addrid  11399  2p2e4  12352  1p2e3  12360  3p2e5  12368  3p3e6  12369  4p2e6  12370  4p3e7  12371  4p4e8  12372  5p2e7  12373  5p3e8  12374  5p4e9  12375  6p2e8  12376  6p3e9  12377  7p2e9  12378  numsuc  12696  nummac  12727  numaddc  12730  6p5lem  12752  5p5e10  12753  6p4e10  12754  7p3e10  12757  8p2e10  12762  binom2i  14181  faclbnd4lem1  14258  3dvdsdec  16280  3dvds2dec  16281  gcdaddmlem  16470  mod2xnegi  17009  decexp2  17013  decsplit  17021  lgsdir2lem2  27066  2lgsoddprmlem3d  27153  ax5seglem7  28461  normlem3  30633  stadd3i  31769  dfdec100  32304  dp3mul10  32332  dpmul  32347  dpmul4  32348  quad3  34954  addassnni  41157  sn-1ne2  41482  sqmid3api  41498  re1m1e0m0  41573  sn-0tie0  41615  fltnltalem  41707  unitadd  43250  sqwvfoura  45243  sqwvfourb  45244  fouriersw  45246  3exp4mod41  46583  bgoldbtbndlem1  46772
  Copyright terms: Public domain W3C validator