Theorem addass 10215

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1072   = wceq 1632   ∈ wcel 2139  (class class class)co 6813  ℂcc 10126   + caddc 10131

This theorem was proved from axioms:  ax-addass 10193

This theorem is referenced by:  addassi  10240  addassd  10254  00id  10403  addid2  10411  add12  10445  add32  10446  add32r  10447  add4  10448  nnaddcl  11234  uzaddcl  11937  xaddass  12272  fztp  12590  seradd  13037  expadd  13096  bernneq  13184  faclbnd6  13280  hashgadd  13358  swrds2  13885  clim2ser  14584  clim2ser2  14585  summolem3  14644  isumsplit  14771  fsumcube  14990  odd2np1lem  15266  prmlem0  16014  cnaddablx  18471  cnaddabl  18472  zaddablx  18475  cncrng  19969  cnlmod  23140  pjthlem1  23408  ptolemy  24447  bcp1ctr  25203  cnaddabloOLD  27745  pjhthlem1  28559  dnibndlem5  32778  mblfinlem2  33760  mogoldbblem  42139  nnsgrp  42327  2zrngasgrp  42450