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

Theorem addassd 7106
Description: Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypotheses
Ref Expression
addcld.1 (𝜑𝐴 ∈ ℂ)
addcld.2 (𝜑𝐵 ∈ ℂ)
addassd.3 (𝜑𝐶 ∈ ℂ)
Assertion
Ref Expression
addassd (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Proof of Theorem addassd
StepHypRef Expression
1 addcld.1 . 2 (𝜑𝐴 ∈ ℂ)
2 addcld.2 . 2 (𝜑𝐵 ∈ ℂ)
3 addassd.3 . 2 (𝜑𝐶 ∈ ℂ)
4 addass 7068 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4syl3anc 1146 1 (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1259  wcel 1409  (class class class)co 5539  cc 6944   + caddc 6949
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 7043
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  readdcan  7213  muladd11r  7229  cnegexlem1  7248  cnegex  7251  addcan  7253  addcan2  7254  negeu  7264  addsubass  7283  nppcan3  7297  muladd  7452  ltadd2  7487  add1p1  8230  div4p1lem1div2  8234  peano2z  8337  zaddcllempos  8338  zpnn0elfzo1  9165  qbtwnzlemstep  9204  rebtwn2zlemstep  9208  flhalf  9251  flqdiv  9270  binom2  9528  binom3  9533  bernneq  9536  cvg1nlemres  9811  recvguniqlem  9820  resqrexlemover  9836
  Copyright terms: Public domain W3C validator