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

Theorem addassd 8011
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 7972 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4syl3anc 1249 1 (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1364  wcel 2160  (class class class)co 5897  cc 7840   + caddc 7845
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-addass 7944
This theorem depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  readdcan  8128  muladd11r  8144  cnegexlem1  8163  cnegex  8166  addcan  8168  addcan2  8169  negeu  8179  addsubass  8198  nppcan3  8212  muladd  8372  ltadd2  8407  add1p1  9199  div4p1lem1div2  9203  peano2z  9320  zaddcllempos  9321  zpnn0elfzo1  10240  exbtwnzlemstep  10280  rebtwn2zlemstep  10285  flhalf  10335  flqdiv  10354  binom2  10666  binom3  10672  bernneq  10675  omgadd  10817  cvg1nlemres  11029  recvguniqlem  11038  resqrexlemover  11054  bdtrilem  11282  bdtri  11283  bcxmas  11532  efsep  11734  efi4p  11760  efival  11775  divalglemnqt  11960  flodddiv4  11974  gcdaddm  12020  pcadd2  12376  4sqlem11  12436  limcimolemlt  14610  tangtx  14736  binom4  14874
  Copyright terms: Public domain W3C validator