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

Theorem addass 7862
Description: Alias for ax-addass 7834, for naming consistency with addassi 7886. (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 7834 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 963    = wceq 1335    e. wcel 2128  (class class class)co 5824   CCcc 7730    + caddc 7735
This theorem was proved from axioms:  ax-addass 7834
This theorem is referenced by:  addassi  7886  addassd  7900  add12  8033  add32  8034  add32r  8035  add4  8036  nnaddcl  8853  uzaddcl  9497  xaddass  9773  fztp  9980  ser3add  10404  expadd  10461  bernneq  10538  faclbnd6  10618  resqrexlemover  10910  clim2ser  11234  clim2ser2  11235  summodclem3  11277  isumsplit  11388  cvgratnnlemseq  11423  odd2np1lem  11763  ptolemy  13156
  Copyright terms: Public domain W3C validator