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

Theorem addassd 7489
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 7451 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4syl3anc 1174 1 (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289  wcel 1438  (class class class)co 5634  cc 7327   + caddc 7332
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 7426
This theorem depends on definitions:  df-bi 115  df-3an 926
This theorem is referenced by:  readdcan  7601  muladd11r  7617  cnegexlem1  7636  cnegex  7639  addcan  7641  addcan2  7642  negeu  7652  addsubass  7671  nppcan3  7685  muladd  7841  ltadd2  7876  add1p1  8635  div4p1lem1div2  8639  peano2z  8756  zaddcllempos  8757  zpnn0elfzo1  9584  exbtwnzlemstep  9624  rebtwn2zlemstep  9629  flhalf  9674  flqdiv  9693  binom2  10030  binom3  10036  bernneq  10039  omgadd  10175  cvg1nlemres  10383  recvguniqlem  10392  resqrexlemover  10408  bcxmas  10845  divalglemnqt  11013  flodddiv4  11027  gcdaddm  11068
  Copyright terms: Public domain W3C validator