ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addassi GIF version

Theorem addassi 7093
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 7069 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4mp3an 1243 1 ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Colors of variables: wff set class
Syntax hints:   = wceq 1259  wcel 1409  (class class class)co 5540  cc 6945   + caddc 6950
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-addass 7044
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  2p2e4  8110  3p2e5  8124  3p3e6  8125  4p2e6  8126  4p3e7  8127  4p4e8  8128  5p2e7  8129  5p3e8  8130  5p4e9  8131  6p2e8  8132  6p3e9  8133  7p2e9  8134  numsuc  8440  nummac  8471  numaddc  8474  6p5lem  8496  5p5e10  8497  6p4e10  8498  7p3e10  8501  8p2e10  8506  binom2i  9527  resqrexlemover  9837  3dvdsdec  10176  3dvds2dec  10177
  Copyright terms: Public domain W3C validator