Theorem addass 8009

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2167  (class class class)co 5922  ℂcc 7877   + caddc 7882

This theorem was proved from axioms:  ax-addass 7981

This theorem is referenced by:  addassi  8034  addassd  8049  add12  8184  add32  8185  add32r  8186  add4  8187  nnaddcl  9010  uzaddcl  9660  xaddass  9944  fztp  10153  ser3add  10614  expadd  10673  bernneq  10752  faclbnd6  10836  resqrexlemover  11175  clim2ser  11502  clim2ser2  11503  summodclem3  11545  isumsplit  11656  cvgratnnlemseq  11691  odd2np1lem  12037  cncrng  14125  ptolemy  15060