Theorem addass 10624

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  (class class class)co 7156  ℂcc 10535   + caddc 10540

This theorem was proved from axioms:  ax-addass 10602

This theorem is referenced by:  addassi  10651  addassd  10663  00id  10815  addid2  10823  add12  10857  add32  10858  add32r  10859  add4  10860  nnaddcl  11661  uzaddcl  12305  xaddass  12643  fztp  12964  seradd  13413  expadd  13472  bernneq  13591  faclbnd6  13660  hashgadd  13739  swrds2  14302  clim2ser  15011  clim2ser2  15012  summolem3  15071  isumsplit  15195  fsumcube  15414  odd2np1lem  15689  prmlem0  16439  cnaddablx  18988  cnaddabl  18989  zaddablx  18992  cncrng  20566  cnlmod  23744  pjthlem1  24040  ptolemy  25082  bcp1ctr  25855  cnaddabloOLD  28358  pjhthlem1  29168  dnibndlem5  33821  mblfinlem2  34945  fac2xp3  39114  facp2  39115  2xp3dxp2ge1d  39117  factwoffsmonot  39118  mogoldbblem  43905  nnsgrp  44104  nn0mnd  44106  2zrngasgrp  44231