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

Theorem addassi 10643
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 10616 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4mp3an 1458 1 ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2115  (class class class)co 7145  cc 10527   + caddc 10532
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 10594
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086
This theorem is referenced by:  mul02lem2  10809  addid1  10812  2p2e4  11765  1p2e3  11773  3p2e5  11781  3p3e6  11782  4p2e6  11783  4p3e7  11784  4p4e8  11785  5p2e7  11786  5p3e8  11787  5p4e9  11788  6p2e8  11789  6p3e9  11790  7p2e9  11791  numsuc  12105  nummac  12136  numaddc  12139  6p5lem  12161  5p5e10  12162  6p4e10  12163  7p3e10  12166  8p2e10  12171  binom2i  13575  faclbnd4lem1  13654  3dvdsdec  15677  3dvds2dec  15678  gcdaddmlem  15866  mod2xnegi  16401  decexp2  16405  decsplit  16413  lgsdir2lem2  25906  2lgsoddprmlem3d  25993  ax5seglem7  26725  normlem3  28891  stadd3i  30027  dfdec100  30550  dp3mul10  30578  dpmul  30593  dpmul4  30594  quad3  32938  addassnni  39178  sn-1ne2  39338  sqmid3api  39349  re1m1e0m0  39407  fltnltalem  39471  unitadd  40757  sqwvfoura  42733  sqwvfourb  42734  fouriersw  42736  3exp4mod41  43997  bgoldbtbndlem1  44186
  Copyright terms: Public domain W3C validator