Theorem addass 11209

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1539   ∈ wcel 2107  (class class class)co 7400  ℂcc 11120   + caddc 11125

This theorem was proved from axioms:  ax-addass 11187

This theorem is referenced by:  addassi  11238  addassd  11250  00id  11403  addlid  11411  add12  11446  add32  11447  add32r  11448  add4  11449  nnaddcl  12256  uzaddcl  12913  xaddass  13258  fztp  13587  seradd  14052  expadd  14112  bernneq  14237  faclbnd6  14307  hashgadd  14385  swrds2  14948  clim2ser  15660  clim2ser2  15661  summolem3  15719  isumsplit  15845  fsumcube  16065  odd2np1lem  16346  prmlem0  17112  cnaddablx  19836  cnaddabl  19837  zaddablx  19840  cncrng  21338  cncrngOLD  21339  cnlmod  25078  pjthlem1  25376  ptolemy  26443  bcp1ctr  27228  cnaddabloOLD  30496  pjhthlem1  31306  dnibndlem5  36429  mblfinlem2  37611  facp2  42085  fac2xp3  42181  2xp3dxp2ge1d  42183  factwoffsmonot  42184  mogoldbblem  47660  nnsgrp  48046  nn0mnd  48048  2zrngasgrp  48115