Theorem addass 8028

Description: Alias for ax-addass 8000, for naming consistency with addassi 8053. (Contributed by NM, 10-Mar-2008.)

Assertion

Ref	Expression
addass	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2167  (class class class)co 5925  ℂcc 7896   + caddc 7901

This theorem was proved from axioms:  ax-addass 8000

This theorem is referenced by:  addassi  8053  addassd  8068  add12  8203  add32  8204  add32r  8205  add4  8206  nnaddcl  9029  uzaddcl  9679  xaddass  9963  fztp  10172  ser3add  10633  expadd  10692  bernneq  10771  faclbnd6  10855  resqrexlemover  11194  clim2ser  11521  clim2ser2  11522  summodclem3  11564  isumsplit  11675  cvgratnnlemseq  11710  odd2np1lem  12056  cncrng  14203  ptolemy  15168