Theorem addass 9902

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977  (class class class)co 6549  ℂcc 9813   + caddc 9818

This theorem was proved from axioms:  ax-addass 9880

This theorem is referenced by:  addassi  9927  addassd  9941  00id  10090  addid2  10098  add12  10132  add32  10133  add32r  10134  add4  10135  nnaddcl  10919  uzaddcl  11620  xaddass  11951  fztp  12267  seradd  12705  expadd  12764  bernneq  12852  faclbnd6  12948  hashgadd  13027  swrds2  13533  clim2ser  14233  clim2ser2  14234  summolem3  14292  isumsplit  14411  fsumcube  14630  odd2np1lem  14902  prmlem0  15650  cnaddablx  18094  cnaddabl  18095  zaddablx  18098  cncrng  19586  cnlmod  22748  pjthlem1  23016  ptolemy  24052  bcp1ctr  24804  wlkdvspthlem  26137  cnaddabloOLD  26820  pjhthlem1  27634  dnibndlem5  31642  mblfinlem2  32617  nnsgrp  41607  2zrngasgrp  41730