Theorem addass 11008

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1539   ∈ wcel 2104  (class class class)co 7307  ℂcc 10919   + caddc 10924

This theorem was proved from axioms:  ax-addass 10986

This theorem is referenced by:  addassi  11035  addassd  11047  00id  11200  addid2  11208  add12  11242  add32  11243  add32r  11244  add4  11245  nnaddcl  12046  uzaddcl  12694  xaddass  13033  fztp  13362  seradd  13815  expadd  13875  bernneq  13994  faclbnd6  14063  hashgadd  14141  swrds2  14702  clim2ser  15415  clim2ser2  15416  summolem3  15475  isumsplit  15601  fsumcube  15819  odd2np1lem  16098  prmlem0  16856  cnaddablx  19518  cnaddabl  19519  zaddablx  19522  cncrng  20668  cnlmod  24352  pjthlem1  24650  ptolemy  25702  bcp1ctr  26476  cnaddabloOLD  28992  pjhthlem1  29802  dnibndlem5  34711  mblfinlem2  35863  facp2  40299  fac2xp3  40360  2xp3dxp2ge1d  40362  factwoffsmonot  40363  mogoldbblem  45416  nnsgrp  45615  nn0mnd  45617  2zrngasgrp  45742