ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  addass Unicode version

Theorem addass 7472
Description: Alias for ax-addass 7447, for naming consistency with addassi 7496. (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 7447 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 924    = wceq 1289    e. wcel 1438  (class class class)co 5652   CCcc 7348    + caddc 7353
This theorem was proved from axioms:  ax-addass 7447
This theorem is referenced by:  addassi  7496  addassd  7510  add12  7640  add32  7641  add32r  7642  add4  7643  nnaddcl  8442  uzaddcl  9074  fztp  9492  iseradd  9934  expadd  9997  bernneq  10074  faclbnd6  10152  resqrexlemover  10443  clim2ser  10725  clim2ser2  10726  isummolem3  10770  isumsplit  10885  cvgratnnlemseq  10920  odd2np1lem  11150
  Copyright terms: Public domain W3C validator