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

Theorem addass 9508
Description: Alias for ax-addass 9486, for naming consistency with addassi 9533. (Contributed by NM, 10-Mar-2008.)
Assertion
Ref Expression
addass  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )

Proof of Theorem addass
StepHypRef Expression
1 ax-addass 9486 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 971    = wceq 1399    e. wcel 1836  (class class class)co 6214   CCcc 9419    + caddc 9424
This theorem was proved from axioms:  ax-addass 9486
This theorem is referenced by:  addassi  9533  addassd  9547  00id  9684  addid2  9692  add12  9722  add32  9723  add32r  9724  add4  9725  nnaddcl  10492  uzaddcl  11075  xaddass  11380  fztp  11676  seradd  12071  expadd  12130  bernneq  12213  faclbnd6  12298  hashgadd  12367  swrds2  12813  clim2ser  13498  clim2ser2  13499  summolem3  13557  isumsplit  13673  odd2np1lem  14066  prmlem0  14612  cnaddablx  17010  cnaddabl  17011  zaddablx  17012  cncrng  18571  pjthlem1  21956  ptolemy  22993  bcp1ctr  23690  wlkdvspthlem  24751  gxnn0add  25414  cnaddablo  25490  pjhthlem1  26447  fsumcube  30011  mblfinlem2  30253  nnsgrp  32858  2zrngasgrp  32981
  Copyright terms: Public domain W3C validator