Theorem addass 9879

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1030   = wceq 1474   ∈ wcel 1976  (class class class)co 6527  ℂcc 9790   + caddc 9795

This theorem was proved from axioms:  ax-addass 9857

This theorem is referenced by:  addassi  9904  addassd  9918  00id  10062  addid2  10070  add12  10104  add32  10105  add32r  10106  add4  10107  nnaddcl  10889  uzaddcl  11576  xaddass  11908  fztp  12222  seradd  12660  expadd  12719  bernneq  12807  faclbnd6  12903  hashgadd  12979  swrds2  13479  clim2ser  14179  clim2ser2  14180  summolem3  14238  isumsplit  14357  fsumcube  14576  odd2np1lem  14848  prmlem0  15596  cnaddablx  18040  cnaddabl  18041  zaddablx  18044  cncrng  19532  cnlmod  22677  pjthlem1  22933  ptolemy  23969  bcp1ctr  24721  wlkdvspthlem  25903  cnaddabloOLD  26604  pjhthlem1  27440  dnibndlem5  31448  mblfinlem2  32413  nnsgrp  41602  2zrngasgrp  41725