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

Theorem addassd 7712
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 7674 . 2 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
51, 2, 3, 4syl3anc 1199 1 (𝜑 → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314  wcel 1463  (class class class)co 5728  cc 7545   + caddc 7550
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-addass 7647
This theorem depends on definitions:  df-bi 116  df-3an 947
This theorem is referenced by:  readdcan  7825  muladd11r  7841  cnegexlem1  7860  cnegex  7863  addcan  7865  addcan2  7866  negeu  7876  addsubass  7895  nppcan3  7909  muladd  8065  ltadd2  8100  add1p1  8873  div4p1lem1div2  8877  peano2z  8994  zaddcllempos  8995  zpnn0elfzo1  9878  exbtwnzlemstep  9918  rebtwn2zlemstep  9923  flhalf  9968  flqdiv  9987  binom2  10296  binom3  10302  bernneq  10305  omgadd  10441  cvg1nlemres  10649  recvguniqlem  10658  resqrexlemover  10674  bdtrilem  10902  bdtri  10903  bcxmas  11150  efsep  11248  efi4p  11275  efival  11290  divalglemnqt  11465  flodddiv4  11479  gcdaddm  11520  limcimolemlt  12589
  Copyright terms: Public domain W3C validator