Theorem addass 8140

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1002   = wceq 1395   ∈ wcel 2200  (class class class)co 6007  ℂcc 8008   + caddc 8013

This theorem was proved from axioms:  ax-addass 8112

This theorem is referenced by:  addassi  8165  addassd  8180  add12  8315  add32  8316  add32r  8317  add4  8318  nnaddcl  9141  uzaddcl  9793  xaddass  10077  fztp  10286  ser3add  10756  expadd  10815  bernneq  10894  faclbnd6  10978  resqrexlemover  11536  clim2ser  11863  clim2ser2  11864  summodclem3  11906  isumsplit  12017  cvgratnnlemseq  12052  odd2np1lem  12398  cncrng  14548  ptolemy  15513