Theorem addass 7750

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 962   = wceq 1331   ∈ wcel 1480  (class class class)co 5774  ℂcc 7618   + caddc 7623

This theorem was proved from axioms:  ax-addass 7722

This theorem is referenced by:  addassi  7774  addassd  7788  add12  7920  add32  7921  add32r  7922  add4  7923  nnaddcl  8740  uzaddcl  9381  xaddass  9652  fztp  9858  ser3add  10278  expadd  10335  bernneq  10412  faclbnd6  10490  resqrexlemover  10782  clim2ser  11106  clim2ser2  11107  summodclem3  11149  isumsplit  11260  cvgratnnlemseq  11295  odd2np1lem  11569  ptolemy  12905