Theorem addass 11088

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2111  (class class class)co 7341  ℂcc 10999   + caddc 11004

This theorem was proved from axioms:  ax-addass 11066

This theorem is referenced by:  addassi  11117  addassd  11129  00id  11283  addlid  11291  add12  11326  add32  11327  add32r  11328  add4  11329  nnaddcl  12143  uzaddcl  12797  xaddass  13143  fztp  13475  seradd  13946  expadd  14006  bernneq  14131  faclbnd6  14201  hashgadd  14279  swrds2  14842  clim2ser  15557  clim2ser2  15558  summolem3  15616  isumsplit  15742  fsumcube  15962  odd2np1lem  16246  prmlem0  17012  cnaddablx  19775  cnaddabl  19776  zaddablx  19779  cncrng  21320  cncrngOLD  21321  cnlmod  25062  pjthlem1  25359  ptolemy  26427  bcp1ctr  27212  cnaddabloOLD  30553  pjhthlem1  31363  dnibndlem5  36516  mblfinlem2  37698  facp2  42176  mogoldbblem  47751  nnsgrp  48208  nn0mnd  48210  2zrngasgrp  48277