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

Step	Hyp	Ref	Expression
1		ax-addass 7641	1 ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

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