Theorem addass 11162

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  (class class class)co 7390  ℂcc 11073   + caddc 11078

This theorem was proved from axioms:  ax-addass 11140

This theorem is referenced by:  addassi  11191  addassd  11203  00id  11356  addlid  11364  add12  11399  add32  11400  add32r  11401  add4  11402  nnaddcl  12216  uzaddcl  12870  xaddass  13216  fztp  13548  seradd  14016  expadd  14076  bernneq  14201  faclbnd6  14271  hashgadd  14349  swrds2  14913  clim2ser  15628  clim2ser2  15629  summolem3  15687  isumsplit  15813  fsumcube  16033  odd2np1lem  16317  prmlem0  17083  cnaddablx  19805  cnaddabl  19806  zaddablx  19809  cncrng  21307  cncrngOLD  21308  cnlmod  25047  pjthlem1  25344  ptolemy  26412  bcp1ctr  27197  cnaddabloOLD  30517  pjhthlem1  31327  dnibndlem5  36477  mblfinlem2  37659  facp2  42138  mogoldbblem  47725  nnsgrp  48169  nn0mnd  48171  2zrngasgrp  48238