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

Theorem addid2i 8114
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 addlid 8110 . 2  |-  ( A  e.  CC  ->  (
0  +  A )  =  A )
31, 2ax-mp 5 1  |-  ( 0  +  A )  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1363    e. wcel 2158  (class class class)co 5888   CCcc 7823   0cc0 7825    + caddc 7828
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1457  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-4 1520  ax-17 1536  ax-ial 1544  ax-ext 2169  ax-1cn 7918  ax-icn 7920  ax-addcl 7921  ax-mulcl 7923  ax-addcom 7925  ax-i2m1 7930  ax-0id 7933
This theorem depends on definitions:  df-bi 117  df-cleq 2180  df-clel 2183
This theorem is referenced by:  ine0  8365  inelr  8555  muleqadd  8639  0p1e1  9047  iap0  9156  num0h  9409  nummul1c  9446  decrmac  9455  decmul1  9461  fz0tp  10136  fz0to4untppr  10138  fzo0to3tp  10233  rei  10922  imi  10923  resqrexlemover  11033  ef01bndlem  11778  efhalfpi  14573  sinq34lt0t  14605  ex-fac  14833
  Copyright terms: Public domain W3C validator