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

Theorem addid1d 7568
Description:  0 is an additive identity. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
addid1d  |-  ( ph  ->  ( A  +  0 )  =  A )

Proof of Theorem addid1d
StepHypRef Expression
1 muld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addid1 7557 . 2  |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )
31, 2syl 14 1  |-  ( ph  ->  ( A  +  0 )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1287    e. wcel 1436  (class class class)co 5607   CCcc 7285   0cc0 7287    + caddc 7290
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-0id 7390
This theorem is referenced by:  subsub2  7647  negsub  7667  ltaddneg  7839  ltaddpos  7867  addge01  7887  add20  7889  apreap  7998  nnge1  8373  nnnn0addcl  8629  un0addcl  8632  peano2z  8712  zaddcl  8716  uzaddcl  8999  fzosubel3  9528  expadd  9888  faclbnd6  10041  omgadd  10099  reim0b  10184  rereb  10185  immul2  10202  resqrexlemcalc3  10337  resqrexlemnm  10339  max0addsup  10540  bezoutlema  10855
  Copyright terms: Public domain W3C validator