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

Theorem addid1d 8109
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 8098 . 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 1353    e. wcel 2148  (class class class)co 5878   CCcc 7812   0cc0 7814    + caddc 7817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-0id 7922
This theorem is referenced by:  subsub2  8188  negsub  8208  ltaddneg  8384  ltaddpos  8412  addge01  8432  add20  8434  apreap  8547  nnge1  8945  nnnn0addcl  9209  un0addcl  9212  peano2z  9292  zaddcl  9296  uzaddcl  9589  xaddid1  9865  fzosubel3  10199  expadd  10565  faclbnd6  10727  omgadd  10785  reim0b  10874  rereb  10875  immul2  10892  resqrexlemcalc3  11028  resqrexlemnm  11030  max0addsup  11231  fsumsplit  11418  sumsplitdc  11443  bezoutlema  12003  pcadd  12342  pcmpt  12344  mulgnn0dir  13019  cosmpi  14377  sinppi  14378  sinhalfpip  14381  trilpolemlt1  14929
  Copyright terms: Public domain W3C validator