Theorem addass 8161

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1004   = wceq 1397   ∈ wcel 2202  (class class class)co 6017  ℂcc 8029   + caddc 8034

This theorem was proved from axioms:  ax-addass 8133

This theorem is referenced by:  addassi  8186  addassd  8201  add12  8336  add32  8337  add32r  8338  add4  8339  nnaddcl  9162  uzaddcl  9819  xaddass  10103  fztp  10312  ser3add  10783  expadd  10842  bernneq  10921  faclbnd6  11005  resqrexlemover  11570  clim2ser  11897  clim2ser2  11898  summodclem3  11940  isumsplit  12051  cvgratnnlemseq  12086  odd2np1lem  12432  cncrng  14582  ptolemy  15547