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

Theorem addid2d 7905
Description:  0 is a left identity for addition. (Contributed by Mario Carneiro, 27-May-2016.)
Hypothesis
Ref Expression
muld.1  |-  ( ph  ->  A  e.  CC )
Assertion
Ref Expression
addid2d  |-  ( ph  ->  ( 0  +  A
)  =  A )

Proof of Theorem addid2d
StepHypRef Expression
1 muld.1 . 2  |-  ( ph  ->  A  e.  CC )
2 addid2 7894 . 2  |-  ( A  e.  CC  ->  (
0  +  A )  =  A )
31, 2syl 14 1  |-  ( ph  ->  ( 0  +  A
)  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331    e. wcel 1480  (class class class)co 5767   CCcc 7611   0cc0 7613    + caddc 7616
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 2119  ax-1cn 7706  ax-icn 7708  ax-addcl 7709  ax-mulcl 7711  ax-addcom 7713  ax-i2m1 7718  ax-0id 7721
This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133
This theorem is referenced by:  negeu  7946  ltadd2  8174  subge0  8230  sublt0d  8325  un0addcl  9003  lincmb01cmp  9779  modsumfzodifsn  10162  rennim  10767  max0addsup  10984  fsumsplit  11169  sumsplitdc  11194  fisum0diag2  11209  isumsplit  11253  arisum2  11261  efaddlem  11369  eftlub  11385  ef4p  11389  moddvds  11491  gcdaddm  11661  gcdmultipled  11670  bezoutlemb  11677  limcimolemlt  12791  dvcnp2cntop  12821  dvmptcmulcn  12841  dveflem  12844  dvef  12845  sin0pilem1  12851  sin2kpi  12881  cos2kpi  12882  coshalfpim  12893  sinkpi  12917
  Copyright terms: Public domain W3C validator