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 1092   = wceq 1547   ∈ wcel 2119  (class class class)co 7356  ℂ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  21368  cnlmod  25125  pjthlem1  25422  ptolemy  26478  bcp1ctr  27260  cnaddabloOLD  30670  pjhthlem1  31480  dnibndlem5  36788  mblfinlem2  38025  facp2  42628  mogoldbblem  48211  nnsgrp  48668  nn0mnd  48670  2zrngasgrp  48737