Theorem addass 11225

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099  (class class class)co 7420  ℂcc 11136   + caddc 11141

This theorem was proved from axioms:  ax-addass 11203

This theorem is referenced by:  addassi  11254  addassd  11266  00id  11419  addlid  11427  add12  11461  add32  11462  add32r  11463  add4  11464  nnaddcl  12265  uzaddcl  12918  xaddass  13260  fztp  13589  seradd  14041  expadd  14101  bernneq  14223  faclbnd6  14290  hashgadd  14368  swrds2  14923  clim2ser  15633  clim2ser2  15634  summolem3  15692  isumsplit  15818  fsumcube  16036  odd2np1lem  16316  prmlem0  17074  cnaddablx  19822  cnaddabl  19823  zaddablx  19826  cncrng  21315  cncrngOLD  21316  cnlmod  25066  pjthlem1  25364  ptolemy  26430  bcp1ctr  27211  cnaddabloOLD  30390  pjhthlem1  31200  dnibndlem5  35957  mblfinlem2  37131  facp2  41615  fac2xp3  41691  2xp3dxp2ge1d  41693  factwoffsmonot  41694  mogoldbblem  47060  nnsgrp  47239  nn0mnd  47241  2zrngasgrp  47308