Theorem addass 11154

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1097   = wceq 1559   ∈ wcel 2141  (class class class)co 7391  ℂcc 11065   + caddc 11070

This theorem was proved from axioms:  ax-addass 11132

This theorem is referenced by:  addassi  11186  addassd  11198  00id  11352  addlid  11360  add12  11395  add32  11396  add32r  11397  add4  11398  nnaddcl  12227  uzaddcl  12899  xaddass  13246  fztp  13579  seradd  14051  expadd  14111  bernneq  14236  faclbnd6  14306  hashgadd  14384  swrds2  14947  clim2ser  15673  clim2ser2  15674  summolem3  15732  isumsplit  15861  fsumcube  16081  odd2np1lem  16365  prmlem0  17132  cnaddablx  19899  cnaddabl  19900  zaddablx  19903  cncrng  21433  cnlmod  25190  pjthlem1  25487  ptolemy  26549  bcp1ctr  27331  cnaddabloOLD  30741  pjhthlem1  31551  dnibndlem5  36881  mblfinlem2  38118  facp2  42721  mogoldbblem  48303  nnsgrp  48760  nn0mnd  48762  2zrngasgrp  48829