Theorem addass 7908

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 974   = wceq 1349   ∈ wcel 2142  (class class class)co 5857  ℂcc 7776   + caddc 7781

This theorem was proved from axioms:  ax-addass 7880

This theorem is referenced by:  addassi  7932  addassd  7946  add12  8081  add32  8082  add32r  8083  add4  8084  nnaddcl  8902  uzaddcl  9549  xaddass  9830  fztp  10038  ser3add  10465  expadd  10522  bernneq  10600  faclbnd6  10682  resqrexlemover  10978  clim2ser  11304  clim2ser2  11305  summodclem3  11347  isumsplit  11458  cvgratnnlemseq  11493  odd2np1lem  11835  ptolemy  13624