Theorem addass 11113

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  (class class class)co 7358  ℂcc 11024   + caddc 11029

This theorem was proved from axioms:  ax-addass 11091

This theorem is referenced by:  addassi  11142  addassd  11154  00id  11308  addlid  11316  add12  11351  add32  11352  add32r  11353  add4  11354  nnaddcl  12168  uzaddcl  12817  xaddass  13164  fztp  13496  seradd  13967  expadd  14027  bernneq  14152  faclbnd6  14222  hashgadd  14300  swrds2  14863  clim2ser  15578  clim2ser2  15579  summolem3  15637  isumsplit  15763  fsumcube  15983  odd2np1lem  16267  prmlem0  17033  cnaddablx  19797  cnaddabl  19798  zaddablx  19801  cncrng  21343  cncrngOLD  21344  cnlmod  25096  pjthlem1  25393  ptolemy  26461  bcp1ctr  27246  cnaddabloOLD  30656  pjhthlem1  31466  dnibndlem5  36682  mblfinlem2  37859  facp2  42397  mogoldbblem  47966  nnsgrp  48423  nn0mnd  48425  2zrngasgrp  48492