Theorem addass 8205

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1005   = wceq 1398   ∈ wcel 2202  (class class class)co 6028  ℂcc 8073   + caddc 8078

This theorem was proved from axioms:  ax-addass 8177

This theorem is referenced by:  addassi  8230  addassd  8244  add12  8379  add32  8380  add32r  8381  add4  8382  nnaddcl  9205  uzaddcl  9864  xaddass  10148  fztp  10358  ser3add  10830  expadd  10889  bernneq  10968  faclbnd6  11052  resqrexlemover  11633  clim2ser  11960  clim2ser2  11961  summodclem3  12004  isumsplit  12115  cvgratnnlemseq  12150  odd2np1lem  12496  cncrng  14648  ptolemy  15618