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

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

Proof of Theorem addass
StepHypRef Expression
1 ax-addass 7426 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff set class
Syntax hints:  wi 4  w3a 924   = wceq 1289  wcel 1438  (class class class)co 5634  cc 7327   + caddc 7332
This theorem was proved from axioms:  ax-addass 7426
This theorem is referenced by:  addassi  7475  addassd  7489  add12  7619  add32  7620  add32r  7621  add4  7622  nnaddcl  8414  uzaddcl  9043  fztp  9459  iseradd  9899  expadd  9962  bernneq  10039  faclbnd6  10117  resqrexlemover  10408  clim2ser  10689  clim2ser2  10690  isummolem3  10734  isumsplit  10847  cvgratnnlemseq  10881  odd2np1lem  10965
  Copyright terms: Public domain W3C validator