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

Theorem addid1d 7834
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 7823 . 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 1314    e. wcel 1463  (class class class)co 5728   CCcc 7545   0cc0 7547    + caddc 7550
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-0id 7653
This theorem is referenced by:  subsub2  7913  negsub  7933  ltaddneg  8105  ltaddpos  8133  addge01  8153  add20  8155  apreap  8267  nnge1  8653  nnnn0addcl  8911  un0addcl  8914  peano2z  8994  zaddcl  8998  uzaddcl  9283  xaddid1  9538  fzosubel3  9866  expadd  10228  faclbnd6  10383  omgadd  10441  reim0b  10527  rereb  10528  immul2  10545  resqrexlemcalc3  10680  resqrexlemnm  10682  max0addsup  10883  fsumsplit  11068  sumsplitdc  11093  bezoutlema  11533  trilpolemlt1  12926
  Copyright terms: Public domain W3C validator