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

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

Proof of Theorem addass
StepHypRef Expression
1 ax-addass 9857 1 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  w3a 1030   = wceq 1474  wcel 1976  (class class class)co 6527  cc 9790   + caddc 9795
This theorem was proved from axioms:  ax-addass 9857
This theorem is referenced by:  addassi  9904  addassd  9918  00id  10062  addid2  10070  add12  10104  add32  10105  add32r  10106  add4  10107  nnaddcl  10889  uzaddcl  11576  xaddass  11908  fztp  12222  seradd  12660  expadd  12719  bernneq  12807  faclbnd6  12903  hashgadd  12979  swrds2  13479  clim2ser  14179  clim2ser2  14180  summolem3  14238  isumsplit  14357  fsumcube  14576  odd2np1lem  14848  prmlem0  15596  cnaddablx  18040  cnaddabl  18041  zaddablx  18044  cncrng  19532  cnlmod  22677  pjthlem1  22933  ptolemy  23969  bcp1ctr  24721  wlkdvspthlem  25903  cnaddabloOLD  26604  pjhthlem1  27440  dnibndlem5  31448  mblfinlem2  32413  nnsgrp  41602  2zrngasgrp  41725
  Copyright terms: Public domain W3C validator