Theorem addass 11116

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  (class class class)co 7360  ℂcc 11027   + caddc 11032

This theorem was proved from axioms:  ax-addass 11094

This theorem is referenced by:  addassi  11146  addassd  11158  00id  11312  addlid  11320  add12  11355  add32  11356  add32r  11357  add4  11358  nnaddcl  12188  uzaddcl  12845  xaddass  13192  fztp  13525  seradd  13997  expadd  14057  bernneq  14182  faclbnd6  14252  hashgadd  14330  swrds2  14893  clim2ser  15608  clim2ser2  15609  summolem3  15667  isumsplit  15796  fsumcube  16016  odd2np1lem  16300  prmlem0  17067  cnaddablx  19834  cnaddabl  19835  zaddablx  19838  cncrng  21378  cncrngOLD  21379  cnlmod  25117  pjthlem1  25414  ptolemy  26473  bcp1ctr  27256  cnaddabloOLD  30667  pjhthlem1  31477  dnibndlem5  36758  mblfinlem2  37993  facp2  42596  mogoldbblem  48208  nnsgrp  48665  nn0mnd  48667  2zrngasgrp  48734