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

Theorem addassi 7886
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 7862 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4mp3an 1319 1 ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Colors of variables: wff set class
Syntax hints:   = wceq 1335  wcel 2128  (class class class)co 5824  cc 7730   + caddc 7735
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-addass 7834
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  2p2e4  8960  3p2e5  8974  3p3e6  8975  4p2e6  8976  4p3e7  8977  4p4e8  8978  5p2e7  8979  5p3e8  8980  5p4e9  8981  6p2e8  8982  6p3e9  8983  7p2e9  8984  numsuc  9308  nummac  9339  numaddc  9342  6p5lem  9364  5p5e10  9365  6p4e10  9366  7p3e10  9369  8p2e10  9374  binom2i  10527  resqrexlemover  10910  3dvdsdec  11756  3dvds2dec  11757
  Copyright terms: Public domain W3C validator