Theorem addass 8152

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1002   = wceq 1395   ∈ wcel 2200  (class class class)co 6013  ℂcc 8020   + caddc 8025

This theorem was proved from axioms:  ax-addass 8124

This theorem is referenced by:  addassi  8177  addassd  8192  add12  8327  add32  8328  add32r  8329  add4  8330  nnaddcl  9153  uzaddcl  9810  xaddass  10094  fztp  10303  ser3add  10774  expadd  10833  bernneq  10912  faclbnd6  10996  resqrexlemover  11561  clim2ser  11888  clim2ser2  11889  summodclem3  11931  isumsplit  12042  cvgratnnlemseq  12077  odd2np1lem  12423  cncrng  14573  ptolemy  15538