Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 0p1e1 | Unicode version |
Description: 0 + 1 = 1. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Ref | Expression |
---|---|
0p1e1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1cn 7837 | . 2 | |
2 | 1 | addid2i 8032 | 1 |
Colors of variables: wff set class |
Syntax hints: wceq 1342 (class class class)co 5836 cc0 7744 c1 7745 caddc 7747 |
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 1434 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-4 1497 ax-17 1513 ax-ial 1521 ax-ext 2146 ax-1cn 7837 ax-icn 7839 ax-addcl 7840 ax-mulcl 7842 ax-addcom 7844 ax-i2m1 7849 ax-0id 7852 |
This theorem depends on definitions: df-bi 116 df-cleq 2157 df-clel 2160 |
This theorem is referenced by: fv0p1e1 8963 zgt0ge1 9240 nn0lt10b 9262 gtndiv 9277 nn0ind-raph 9299 1e0p1 9354 fz01en 9978 fz01or 10036 fz0tp 10047 fz0to3un2pr 10048 elfzonlteqm1 10135 fzo0to2pr 10143 fzo0to3tp 10144 fldiv4p1lem1div2 10230 mulp1mod1 10290 1tonninf 10365 expp1 10452 facp1 10632 faclbnd 10643 bcm1k 10662 bcval5 10665 bcpasc 10668 hash1 10713 binomlem 11410 isumnn0nn 11420 fprodfac 11542 ege2le3 11598 ef4p 11621 eirraplem 11703 p1modz1 11720 nn0o1gt2 11827 pw2dvdslemn 12076 pcfaclem 12258 ennnfonelemjn 12278 exmidunben 12302 012of 13716 2o01f 13717 isomninnlem 13750 iswomninnlem 13769 ismkvnnlem 13772 |
Copyright terms: Public domain | W3C validator |