Theorem addass 8037

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1372   ∈ wcel 2175  (class class class)co 5934  ℂcc 7905   + caddc 7910

This theorem was proved from axioms:  ax-addass 8009

This theorem is referenced by:  addassi  8062  addassd  8077  add12  8212  add32  8213  add32r  8214  add4  8215  nnaddcl  9038  uzaddcl  9689  xaddass  9973  fztp  10182  ser3add  10648  expadd  10707  bernneq  10786  faclbnd6  10870  resqrexlemover  11240  clim2ser  11567  clim2ser2  11568  summodclem3  11610  isumsplit  11721  cvgratnnlemseq  11756  odd2np1lem  12102  cncrng  14249  ptolemy  15214