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

Theorem addassi 7494
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 7470 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4mp3an 1273 1 ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Colors of variables: wff set class
Syntax hints:   = wceq 1289  wcel 1438  (class class class)co 5652  cc 7346   + caddc 7351
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-addass 7445
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  2p2e4  8541  3p2e5  8555  3p3e6  8556  4p2e6  8557  4p3e7  8558  4p4e8  8559  5p2e7  8560  5p3e8  8561  5p4e9  8562  6p2e8  8563  6p3e9  8564  7p2e9  8565  numsuc  8888  nummac  8919  numaddc  8922  6p5lem  8944  5p5e10  8945  6p4e10  8946  7p3e10  8949  8p2e10  8954  binom2i  10059  resqrexlemover  10439  3dvdsdec  11139  3dvds2dec  11140
  Copyright terms: Public domain W3C validator