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

Theorem addassi 11302
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 11273 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4mp3an 1461 1 ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1537  wcel 2108  (class class class)co 7450  cc 11184   + caddc 11189
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 11251
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089
This theorem is referenced by:  mul02lem2  11469  addrid  11472  2p2e4  12430  1p2e3  12438  3p2e5  12446  3p3e6  12447  4p2e6  12448  4p3e7  12449  4p4e8  12450  5p2e7  12451  5p3e8  12452  5p4e9  12453  6p2e8  12454  6p3e9  12455  7p2e9  12456  numsuc  12774  nummac  12805  numaddc  12808  6p5lem  12830  5p5e10  12831  6p4e10  12832  7p3e10  12835  8p2e10  12840  binom2i  14263  faclbnd4lem1  14344  3dvdsdec  16382  3dvds2dec  16383  gcdaddmlem  16572  mod2xnegi  17120  decexp2  17124  decsplit  17132  lgsdir2lem2  27390  2lgsoddprmlem3d  27477  ax5seglem7  28970  normlem3  31146  stadd3i  32282  dfdec100  32836  dp3mul10  32864  dpmul  32879  dpmul4  32880  quad3  35640  addassnni  41943  sn-1ne2  42256  sqmid3api  42274  re1m1e0m0  42375  sn-0tie0  42417  fltnltalem  42619  unitadd  44159  sqwvfoura  46151  sqwvfourb  46152  fouriersw  46154  3exp4mod41  47492  bgoldbtbndlem1  47681
  Copyright terms: Public domain W3C validator