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

Theorem addassi 10639
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 10612 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4mp3an 1452 1 ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105  (class class class)co 7145  cc 10523   + caddc 10528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-addass 10590
This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1081
This theorem is referenced by:  mul02lem2  10805  addid1  10808  2p2e4  11760  1p2e3  11768  3p2e5  11776  3p3e6  11777  4p2e6  11778  4p3e7  11779  4p4e8  11780  5p2e7  11781  5p3e8  11782  5p4e9  11783  6p2e8  11784  6p3e9  11785  7p2e9  11786  numsuc  12100  nummac  12131  numaddc  12134  6p5lem  12156  5p5e10  12157  6p4e10  12158  7p3e10  12161  8p2e10  12166  binom2i  13562  faclbnd4lem1  13641  3dvdsdec  15669  3dvds2dec  15670  gcdaddmlem  15860  mod2xnegi  16395  decexp2  16399  decsplit  16407  lgsdir2lem2  25829  2lgsoddprmlem3d  25916  ax5seglem7  26648  normlem3  28816  stadd3i  29952  dfdec100  30473  dp3mul10  30501  dpmul  30516  dpmul4  30517  quad3  32810  sn-1ne2  39036  sqmid3api  39047  re1m1e0m0  39105  fltnltalem  39152  unitadd  40426  sqwvfoura  42390  sqwvfourb  42391  fouriersw  42393  3exp4mod41  43658  bgoldbtbndlem1  43847
  Copyright terms: Public domain W3C validator