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

Theorem addid2i 7912
Description:  0 is a left identity for addition. (Contributed by NM, 3-Jan-2013.)
Hypothesis
Ref Expression
mul.1  |-  A  e.  CC
Assertion
Ref Expression
addid2i  |-  ( 0  +  A )  =  A

Proof of Theorem addid2i
StepHypRef Expression
1 mul.1 . 2  |-  A  e.  CC
2 addid2 7908 . 2  |-  ( A  e.  CC  ->  (
0  +  A )  =  A )
31, 2ax-mp 5 1  |-  ( 0  +  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1331    e. wcel 1480  (class class class)co 5774   CCcc 7625   0cc0 7627    + caddc 7630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121  ax-1cn 7720  ax-icn 7722  ax-addcl 7723  ax-mulcl 7725  ax-addcom 7727  ax-i2m1 7732  ax-0id 7735
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  ine0  8163  inelr  8353  muleqadd  8436  0p1e1  8841  iap0  8950  num0h  9200  nummul1c  9237  decrmac  9246  decmul1  9252  fz0tp  9908  fzo0to3tp  10003  rei  10678  imi  10679  resqrexlemover  10789  ef01bndlem  11470  efhalfpi  12893  sinq34lt0t  12925  ex-fac  12970
  Copyright terms: Public domain W3C validator