Theorem addass 8004

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2164  (class class class)co 5919  ℂcc 7872   + caddc 7877

This theorem was proved from axioms:  ax-addass 7976

This theorem is referenced by:  addassi  8029  addassd  8044  add12  8179  add32  8180  add32r  8181  add4  8182  nnaddcl  9004  uzaddcl  9654  xaddass  9938  fztp  10147  ser3add  10596  expadd  10655  bernneq  10734  faclbnd6  10818  resqrexlemover  11157  clim2ser  11483  clim2ser2  11484  summodclem3  11526  isumsplit  11637  cvgratnnlemseq  11672  odd2np1lem  12016  cncrng  14068  ptolemy  15000