Theorem addass 10613

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  (class class class)co 7135  ℂcc 10524   + caddc 10529

This theorem was proved from axioms:  ax-addass 10591

This theorem is referenced by:  addassi  10640  addassd  10652  00id  10804  addid2  10812  add12  10846  add32  10847  add32r  10848  add4  10849  nnaddcl  11648  uzaddcl  12292  xaddass  12630  fztp  12958  seradd  13408  expadd  13467  bernneq  13586  faclbnd6  13655  hashgadd  13734  swrds2  14293  clim2ser  15003  clim2ser2  15004  summolem3  15063  isumsplit  15187  fsumcube  15406  odd2np1lem  15681  prmlem0  16431  cnaddablx  18981  cnaddabl  18982  zaddablx  18985  cncrng  20112  cnlmod  23745  pjthlem1  24041  ptolemy  25089  bcp1ctr  25863  cnaddabloOLD  28364  pjhthlem1  29174  dnibndlem5  33934  mblfinlem2  35095  facp2  39347  fac2xp3  39385  2xp3dxp2ge1d  39387  factwoffsmonot  39388  mogoldbblem  44238  nnsgrp  44437  nn0mnd  44439  2zrngasgrp  44564