Theorem addass 7856

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 963   = wceq 1335   ∈ wcel 2128  (class class class)co 5821  ℂcc 7724   + caddc 7729

This theorem was proved from axioms:  ax-addass 7828

This theorem is referenced by:  addassi  7880  addassd  7894  add12  8027  add32  8028  add32r  8029  add4  8030  nnaddcl  8847  uzaddcl  9491  xaddass  9766  fztp  9973  ser3add  10397  expadd  10454  bernneq  10531  faclbnd6  10611  resqrexlemover  10903  clim2ser  11227  clim2ser2  11228  summodclem3  11270  isumsplit  11381  cvgratnnlemseq  11416  odd2np1lem  11755  ptolemy  13116