Theorem addass 11131

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109  (class class class)co 7369  ℂcc 11042   + caddc 11047

This theorem was proved from axioms:  ax-addass 11109

This theorem is referenced by:  addassi  11160  addassd  11172  00id  11325  addlid  11333  add12  11368  add32  11369  add32r  11370  add4  11371  nnaddcl  12185  uzaddcl  12839  xaddass  13185  fztp  13517  seradd  13985  expadd  14045  bernneq  14170  faclbnd6  14240  hashgadd  14318  swrds2  14882  clim2ser  15597  clim2ser2  15598  summolem3  15656  isumsplit  15782  fsumcube  16002  odd2np1lem  16286  prmlem0  17052  cnaddablx  19774  cnaddabl  19775  zaddablx  19778  cncrng  21276  cncrngOLD  21277  cnlmod  25016  pjthlem1  25313  ptolemy  26381  bcp1ctr  27166  cnaddabloOLD  30483  pjhthlem1  31293  dnibndlem5  36443  mblfinlem2  37625  facp2  42104  mogoldbblem  47694  nnsgrp  48138  nn0mnd  48140  2zrngasgrp  48207