Theorem addass 8125

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1002   = wceq 1395   ∈ wcel 2200  (class class class)co 6000  ℂcc 7993   + caddc 7998

This theorem was proved from axioms:  ax-addass 8097

This theorem is referenced by:  addassi  8150  addassd  8165  add12  8300  add32  8301  add32r  8302  add4  8303  nnaddcl  9126  uzaddcl  9777  xaddass  10061  fztp  10270  ser3add  10739  expadd  10798  bernneq  10877  faclbnd6  10961  resqrexlemover  11516  clim2ser  11843  clim2ser2  11844  summodclem3  11886  isumsplit  11997  cvgratnnlemseq  12032  odd2np1lem  12378  cncrng  14527  ptolemy  15492