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

Theorem addassi 11246
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 11217 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4mp3an 1458 1 ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1534  wcel 2099  (class class class)co 7414  cc 11128   + caddc 11133
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 11195
This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1087
This theorem is referenced by:  mul02lem2  11413  addrid  11416  2p2e4  12369  1p2e3  12377  3p2e5  12385  3p3e6  12386  4p2e6  12387  4p3e7  12388  4p4e8  12389  5p2e7  12390  5p3e8  12391  5p4e9  12392  6p2e8  12393  6p3e9  12394  7p2e9  12395  numsuc  12713  nummac  12744  numaddc  12747  6p5lem  12769  5p5e10  12770  6p4e10  12771  7p3e10  12774  8p2e10  12779  binom2i  14199  faclbnd4lem1  14276  3dvdsdec  16300  3dvds2dec  16301  gcdaddmlem  16490  mod2xnegi  17031  decexp2  17035  decsplit  17043  lgsdir2lem2  27246  2lgsoddprmlem3d  27333  ax5seglem7  28733  normlem3  30909  stadd3i  32045  dfdec100  32575  dp3mul10  32603  dpmul  32618  dpmul4  32619  quad3  35210  addassnni  41392  sn-1ne2  41762  sqmid3api  41779  re1m1e0m0  41874  sn-0tie0  41916  fltnltalem  42008  unitadd  43548  sqwvfoura  45539  sqwvfourb  45540  fouriersw  45542  3exp4mod41  46879  bgoldbtbndlem1  47068
  Copyright terms: Public domain W3C validator