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

Theorem addid2d 7632
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 7621 . 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 1289    e. wcel 1438  (class class class)co 5652   CCcc 7348   0cc0 7350    + caddc 7353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472  ax-ext 2070  ax-1cn 7438  ax-icn 7440  ax-addcl 7441  ax-mulcl 7443  ax-addcom 7445  ax-i2m1 7450  ax-0id 7453
This theorem depends on definitions:  df-bi 115  df-cleq 2081  df-clel 2084
This theorem is referenced by:  negeu  7673  ltadd2  7897  subge0  7953  sublt0d  8047  un0addcl  8706  lincmb01cmp  9420  modsumfzodifsn  9803  rennim  10435  max0addsup  10652  fsumsplit  10801  sumsplitdc  10826  fisum0diag2  10841  isumsplit  10885  arisum2  10893  efaddlem  10964  eftlub  10980  ef4p  10984  moddvds  11083  gcdaddm  11253  bezoutlemb  11267
  Copyright terms: Public domain W3C validator