Theorem addass 8162

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1004   = wceq 1397   ∈ wcel 2202  (class class class)co 6018  ℂcc 8030   + caddc 8035

This theorem was proved from axioms:  ax-addass 8134

This theorem is referenced by:  addassi  8187  addassd  8202  add12  8337  add32  8338  add32r  8339  add4  8340  nnaddcl  9163  uzaddcl  9820  xaddass  10104  fztp  10313  ser3add  10785  expadd  10844  bernneq  10923  faclbnd6  11007  resqrexlemover  11575  clim2ser  11902  clim2ser2  11903  summodclem3  11946  isumsplit  12057  cvgratnnlemseq  12092  odd2np1lem  12438  cncrng  14589  ptolemy  15554