Theorem addass 11155

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  (class class class)co 7387  ℂcc 11066   + caddc 11071

This theorem was proved from axioms:  ax-addass 11133

This theorem is referenced by:  addassi  11184  addassd  11196  00id  11349  addlid  11357  add12  11392  add32  11393  add32r  11394  add4  11395  nnaddcl  12209  uzaddcl  12863  xaddass  13209  fztp  13541  seradd  14009  expadd  14069  bernneq  14194  faclbnd6  14264  hashgadd  14342  swrds2  14906  clim2ser  15621  clim2ser2  15622  summolem3  15680  isumsplit  15806  fsumcube  16026  odd2np1lem  16310  prmlem0  17076  cnaddablx  19798  cnaddabl  19799  zaddablx  19802  cncrng  21300  cncrngOLD  21301  cnlmod  25040  pjthlem1  25337  ptolemy  26405  bcp1ctr  27190  cnaddabloOLD  30510  pjhthlem1  31320  dnibndlem5  36470  mblfinlem2  37652  facp2  42131  mogoldbblem  47721  nnsgrp  48165  nn0mnd  48167  2zrngasgrp  48234