![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-2 | GIF version |
Description: Define the number 2. (Contributed by NM, 27-May-1999.) |
Ref | Expression |
---|---|
df-2 | ⊢ 2 = (1 + 1) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | c2 8795 | . 2 class 2 | |
2 | c1 7645 | . . 3 class 1 | |
3 | caddc 7647 | . . 3 class + | |
4 | 2, 2, 3 | co 5782 | . 2 class (1 + 1) |
5 | 1, 4 | wceq 1332 | 1 wff 2 = (1 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 2re 8814 0le2 8834 2pos 8835 1p1e2 8861 2p2e4 8871 2times 8872 3p2e5 8885 4p2e6 8887 5p2e7 8890 6p2e8 8893 7p2e9 8895 2nn 8905 1lt2 8913 nneoor 9177 6p6e12 9279 7p5e12 9282 8p2e10 9285 8p4e12 9287 9p2e11 9292 9p3e12 9293 5t2e10 9305 eluz2b1 9422 nn01to3 9436 fztp 9889 fzprval 9893 fztpval 9894 fzo12sn 10025 rebtwn2zlemstep 10061 rebtwn2z 10063 sqval 10382 fac2 10509 bcp1m1 10543 hashprg 10586 binom11 11287 ege2le3 11414 ef4p 11437 efgt1p2 11438 eirraplem 11519 odd2np1lem 11605 opoe 11628 ncoprmgcdne1b 11806 isprm3 11835 prmind2 11837 dvdsnprmd 11842 prmgt1 11848 dveflem 12895 coskpi 12977 ex-fl 13108 |
Copyright terms: Public domain | W3C validator |