Theorem addass 11125

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

Assertion

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

Proof of Theorem addass

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

Syntax hints:   → wi 4   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114  (class class class)co 7367  ℂcc 11036   + caddc 11041

This theorem was proved from axioms:  ax-addass 11103

This theorem is referenced by:  addassi  11155  addassd  11167  00id  11321  addlid  11329  add12  11364  add32  11365  add32r  11366  add4  11367  nnaddcl  12197  uzaddcl  12854  xaddass  13201  fztp  13534  seradd  14006  expadd  14066  bernneq  14191  faclbnd6  14261  hashgadd  14339  swrds2  14902  clim2ser  15617  clim2ser2  15618  summolem3  15676  isumsplit  15805  fsumcube  16025  odd2np1lem  16309  prmlem0  17076  cnaddablx  19843  cnaddabl  19844  zaddablx  19847  cncrng  21373  cnlmod  25107  pjthlem1  25404  ptolemy  26460  bcp1ctr  27242  cnaddabloOLD  30652  pjhthlem1  31462  dnibndlem5  36742  mblfinlem2  37979  facp2  42582  mogoldbblem  48196  nnsgrp  48653  nn0mnd  48655  2zrngasgrp  48722