Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-2 | Unicode version |
Description: Define the number 2. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c2 8771 | . 2 | |
2 | c1 7621 | . . 3 | |
3 | caddc 7623 | . . 3 | |
4 | 2, 2, 3 | co 5774 | . 2 |
5 | 1, 4 | wceq 1331 | 1 |
Colors of variables: wff set class |
This definition is referenced by: 2re 8790 0le2 8810 2pos 8811 1p1e2 8837 2p2e4 8847 2times 8848 3p2e5 8861 4p2e6 8863 5p2e7 8866 6p2e8 8869 7p2e9 8871 2nn 8881 1lt2 8889 nneoor 9153 6p6e12 9255 7p5e12 9258 8p2e10 9261 8p4e12 9263 9p2e11 9268 9p3e12 9269 5t2e10 9281 eluz2b1 9395 nn01to3 9409 fztp 9858 fzprval 9862 fztpval 9863 fzo12sn 9994 rebtwn2zlemstep 10030 rebtwn2z 10032 sqval 10351 fac2 10477 bcp1m1 10511 hashprg 10554 binom11 11255 ege2le3 11377 ef4p 11400 efgt1p2 11401 eirraplem 11483 odd2np1lem 11569 opoe 11592 ncoprmgcdne1b 11770 isprm3 11799 prmind2 11801 dvdsnprmd 11806 prmgt1 11812 dveflem 12855 coskpi 12929 ex-fl 12937 |
Copyright terms: Public domain | W3C validator |