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  8245  add12  8380  add32  8381  add32r  8382  add4  8383  nnaddcl  9206  uzaddcl  9863  xaddass  10147  fztp  10356  ser3add  10828  expadd  10887  bernneq  10966  faclbnd6  11050  resqrexlemover  11631  clim2ser  11958  clim2ser2  11959  summodclem3  12002  isumsplit  12113  cvgratnnlemseq  12148  odd2np1lem  12494  cncrng  14645  ptolemy  15615