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

Theorem addass 9012
Description: Alias for ax-addass 8990, for naming consistency with addassi 9033. (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 8990 1  |-  ( ( A  e.  CC  /\  B  e.  CC  /\  C  e.  CC )  ->  (
( A  +  B
)  +  C )  =  ( A  +  ( B  +  C
) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936    = wceq 1649    e. wcel 1717  (class class class)co 6022   CCcc 8923    + caddc 8928
This theorem is referenced by:  addassi  9033  addassd  9045  00id  9175  addid2  9183  add12  9213  add32  9214  add4  9215  nnaddcl  9956  nneo  10287  uzaddcl  10467  xaddass  10762  fztp  11036  seradd  11294  expadd  11351  bernneq  11434  faclbnd6  11519  hashgadd  11580  swrds2  11809  clim2ser  12377  clim2ser2  12378  summolem3  12437  bcxmaslem2  12543  isumsplit  12549  odd2np1lem  12836  prmlem0  13357  cnaddablx  15410  cnaddabl  15411  zaddablx  15412  cncrng  16647  pjthlem1  19207  ptolemy  20273  bcp1ctr  20932  wlkdvspthlem  21457  gxnn0add  21712  cnaddablo  21788  pjhthlem1  22743  fsumcube  25822
This theorem was proved from axioms:  ax-addass 8990
  Copyright terms: Public domain W3C validator