Theorem addass 11216

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2108  (class class class)co 7405  ℂcc 11127   + caddc 11132

This theorem was proved from axioms:  ax-addass 11194

This theorem is referenced by:  addassi  11245  addassd  11257  00id  11410  addlid  11418  add12  11453  add32  11454  add32r  11455  add4  11456  nnaddcl  12263  uzaddcl  12920  xaddass  13265  fztp  13597  seradd  14062  expadd  14122  bernneq  14247  faclbnd6  14317  hashgadd  14395  swrds2  14959  clim2ser  15671  clim2ser2  15672  summolem3  15730  isumsplit  15856  fsumcube  16076  odd2np1lem  16359  prmlem0  17125  cnaddablx  19849  cnaddabl  19850  zaddablx  19853  cncrng  21351  cncrngOLD  21352  cnlmod  25091  pjthlem1  25389  ptolemy  26457  bcp1ctr  27242  cnaddabloOLD  30562  pjhthlem1  31372  dnibndlem5  36500  mblfinlem2  37682  facp2  42156  fac2xp3  42252  2xp3dxp2ge1d  42254  factwoffsmonot  42255  mogoldbblem  47734  nnsgrp  48152  nn0mnd  48154  2zrngasgrp  48221