Theorem addass 11203

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105  (class class class)co 7412  ℂcc 11114   + caddc 11119

This theorem was proved from axioms:  ax-addass 11181

This theorem is referenced by:  addassi  11231  addassd  11243  00id  11396  addlid  11404  add12  11438  add32  11439  add32r  11440  add4  11441  nnaddcl  12242  uzaddcl  12895  xaddass  13235  fztp  13564  seradd  14017  expadd  14077  bernneq  14199  faclbnd6  14266  hashgadd  14344  swrds2  14898  clim2ser  15608  clim2ser2  15609  summolem3  15667  isumsplit  15793  fsumcube  16011  odd2np1lem  16290  prmlem0  17046  cnaddablx  19784  cnaddabl  19785  zaddablx  19788  cncrng  21255  cnlmod  24987  pjthlem1  25285  ptolemy  26346  bcp1ctr  27126  cnaddabloOLD  30268  pjhthlem1  31078  gg-cncrng  35649  dnibndlem5  35824  mblfinlem2  36992  facp2  41428  fac2xp3  41489  2xp3dxp2ge1d  41491  factwoffsmonot  41492  mogoldbblem  46849  nnsgrp  47016  nn0mnd  47018  2zrngasgrp  47085