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

Theorem addid2 7869
Description:  0 is a left identity for addition. (Contributed by Scott Fenton, 3-Jan-2013.)
Assertion
Ref Expression
addid2  |-  ( A  e.  CC  ->  (
0  +  A )  =  A )

Proof of Theorem addid2
StepHypRef Expression
1 0cn 7726 . . 3  |-  0  e.  CC
2 addcom 7867 . . 3  |-  ( ( A  e.  CC  /\  0  e.  CC )  ->  ( A  +  0 )  =  ( 0  +  A ) )
31, 2mpan2 421 . 2  |-  ( A  e.  CC  ->  ( A  +  0 )  =  ( 0  +  A ) )
4 addid1 7868 . 2  |-  ( A  e.  CC  ->  ( A  +  0 )  =  A )
53, 4eqtr3d 2152 1  |-  ( A  e.  CC  ->  (
0  +  A )  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316    e. wcel 1465  (class class class)co 5742   CCcc 7586   0cc0 7588    + caddc 7591
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 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-4 1472  ax-17 1491  ax-ial 1499  ax-ext 2099  ax-1cn 7681  ax-icn 7683  ax-addcl 7684  ax-mulcl 7686  ax-addcom 7688  ax-i2m1 7693  ax-0id 7696
This theorem depends on definitions:  df-bi 116  df-cleq 2110  df-clel 2113
This theorem is referenced by:  readdcan  7870  addid2i  7873  addid2d  7880  cnegexlem1  7905  cnegexlem2  7906  addcan  7910  negneg  7980  fzoaddel2  9938  divfl0  10037  modqid  10090  sumrbdclem  11113  summodclem2a  11118  fisum0diag2  11184  eftlub  11323  gcdid  11601  ptolemy  12832
  Copyright terms: Public domain W3C validator