Theorem addass 8075

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 981   = wceq 1373   ∈ wcel 2177  (class class class)co 5957  ℂcc 7943   + caddc 7948

This theorem was proved from axioms:  ax-addass 8047

This theorem is referenced by:  addassi  8100  addassd  8115  add12  8250  add32  8251  add32r  8252  add4  8253  nnaddcl  9076  uzaddcl  9727  xaddass  10011  fztp  10220  ser3add  10689  expadd  10748  bernneq  10827  faclbnd6  10911  resqrexlemover  11396  clim2ser  11723  clim2ser2  11724  summodclem3  11766  isumsplit  11877  cvgratnnlemseq  11912  odd2np1lem  12258  cncrng  14406  ptolemy  15371