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

Theorem addassi 7742
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 7718 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4mp3an 1300 1 ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶))
Colors of variables: wff set class
Syntax hints:   = wceq 1316  wcel 1465  (class class class)co 5742  cc 7586   + caddc 7591
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 7690
This theorem depends on definitions:  df-bi 116  df-3an 949
This theorem is referenced by:  2p2e4  8815  3p2e5  8829  3p3e6  8830  4p2e6  8831  4p3e7  8832  4p4e8  8833  5p2e7  8834  5p3e8  8835  5p4e9  8836  6p2e8  8837  6p3e9  8838  7p2e9  8839  numsuc  9163  nummac  9194  numaddc  9197  6p5lem  9219  5p5e10  9220  6p4e10  9221  7p3e10  9224  8p2e10  9229  binom2i  10369  resqrexlemover  10750  3dvdsdec  11489  3dvds2dec  11490
  Copyright terms: Public domain W3C validator