MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  addass Structured version   Visualization version   GIF version

Theorem addass 10215
Description: Alias for ax-addass 10193, for naming consistency with addassi 10240. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addass ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))

Proof of Theorem addass
StepHypRef Expression
1 ax-addass 10193 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1072   = wceq 1632  wcel 2139  (class class class)co 6813  cc 10126   + caddc 10131
This theorem was proved from axioms:  ax-addass 10193
This theorem is referenced by:  addassi  10240  addassd  10254  00id  10403  addid2  10411  add12  10445  add32  10446  add32r  10447  add4  10448  nnaddcl  11234  uzaddcl  11937  xaddass  12272  fztp  12590  seradd  13037  expadd  13096  bernneq  13184  faclbnd6  13280  hashgadd  13358  swrds2  13885  clim2ser  14584  clim2ser2  14585  summolem3  14644  isumsplit  14771  fsumcube  14990  odd2np1lem  15266  prmlem0  16014  cnaddablx  18471  cnaddabl  18472  zaddablx  18475  cncrng  19969  cnlmod  23140  pjthlem1  23408  ptolemy  24447  bcp1ctr  25203  cnaddabloOLD  27745  pjhthlem1  28559  dnibndlem5  32778  mblfinlem2  33760  mogoldbblem  42139  nnsgrp  42327  2zrngasgrp  42450
  Copyright terms: Public domain W3C validator