Theorem addass 11115

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  (class class class)co 7353  ℂcc 11026   + caddc 11031

This theorem was proved from axioms:  ax-addass 11093

This theorem is referenced by:  addassi  11144  addassd  11156  00id  11310  addlid  11318  add12  11353  add32  11354  add32r  11355  add4  11356  nnaddcl  12170  uzaddcl  12824  xaddass  13170  fztp  13502  seradd  13970  expadd  14030  bernneq  14155  faclbnd6  14225  hashgadd  14303  swrds2  14866  clim2ser  15581  clim2ser2  15582  summolem3  15640  isumsplit  15766  fsumcube  15986  odd2np1lem  16270  prmlem0  17036  cnaddablx  19766  cnaddabl  19767  zaddablx  19770  cncrng  21314  cncrngOLD  21315  cnlmod  25057  pjthlem1  25354  ptolemy  26422  bcp1ctr  27207  cnaddabloOLD  30544  pjhthlem1  31354  dnibndlem5  36475  mblfinlem2  37657  facp2  42136  mogoldbblem  47724  nnsgrp  48181  nn0mnd  48183  2zrngasgrp  48250