Theorem addass 7943

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 978   = wceq 1353   ∈ wcel 2148  (class class class)co 5877  ℂcc 7811   + caddc 7816

This theorem was proved from axioms:  ax-addass 7915

This theorem is referenced by:  addassi  7967  addassd  7982  add12  8117  add32  8118  add32r  8119  add4  8120  nnaddcl  8941  uzaddcl  9588  xaddass  9871  fztp  10080  ser3add  10507  expadd  10564  bernneq  10643  faclbnd6  10726  resqrexlemover  11021  clim2ser  11347  clim2ser2  11348  summodclem3  11390  isumsplit  11501  cvgratnnlemseq  11536  odd2np1lem  11879  cncrng  13548  ptolemy  14330