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

Theorem addass 7668
Description: Alias for ax-addass 7641, for naming consistency with addassi 7692. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addass ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Proof of Theorem addass
StepHypRef Expression
1 ax-addass 7641 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 943   = wceq 1312  wcel 1461  (class class class)co 5726  cc 7539   + caddc 7544
This theorem was proved from axioms:  ax-addass 7641
This theorem is referenced by:  addassi  7692  addassd  7706  add12  7837  add32  7838  add32r  7839  add4  7840  nnaddcl  8644  uzaddcl  9277  xaddass  9539  fztp  9745  ser3add  10165  expadd  10222  bernneq  10299  faclbnd6  10377  resqrexlemover  10668  clim2ser  10992  clim2ser2  10993  summodclem3  11035  isumsplit  11146  cvgratnnlemseq  11181  odd2np1lem  11411
  Copyright terms: Public domain W3C validator