Theorem addass 8002

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 980   = wceq 1364   ∈ wcel 2164  (class class class)co 5918  ℂcc 7870   + caddc 7875

This theorem was proved from axioms:  ax-addass 7974

This theorem is referenced by:  addassi  8027  addassd  8042  add12  8177  add32  8178  add32r  8179  add4  8180  nnaddcl  9002  uzaddcl  9651  xaddass  9935  fztp  10144  ser3add  10593  expadd  10652  bernneq  10731  faclbnd6  10815  resqrexlemover  11154  clim2ser  11480  clim2ser2  11481  summodclem3  11523  isumsplit  11634  cvgratnnlemseq  11669  odd2np1lem  12013  cncrng  14057  ptolemy  14959