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 8735 | . 2 class 2 | |
2 | c1 7589 | . . 3 class 1 | |
3 | caddc 7591 | . . 3 class + | |
4 | 2, 2, 3 | co 5742 | . 2 class (1 + 1) |
5 | 1, 4 | wceq 1316 | 1 wff 2 = (1 + 1) |
Colors of variables: wff set class |
This definition is referenced by: 2re 8754 0le2 8774 2pos 8775 1p1e2 8801 2p2e4 8805 2times 8806 3p2e5 8819 4p2e6 8821 5p2e7 8824 6p2e8 8827 7p2e9 8829 2nn 8839 1lt2 8847 nneoor 9111 6p6e12 9213 7p5e12 9216 8p2e10 9219 8p4e12 9221 9p2e11 9226 9p3e12 9227 5t2e10 9239 eluz2b1 9351 nn01to3 9365 fztp 9813 fzprval 9817 fztpval 9818 fzo12sn 9949 rebtwn2zlemstep 9985 rebtwn2z 9987 sqval 10306 fac2 10432 bcp1m1 10466 hashprg 10509 binom11 11210 ege2le3 11291 ef4p 11314 efgt1p2 11315 eirraplem 11395 odd2np1lem 11481 opoe 11504 ncoprmgcdne1b 11682 isprm3 11711 prmind2 11713 dvdsnprmd 11718 prmgt1 11724 dveflem 12766 ex-fl 12833 |
Copyright terms: Public domain | W3C validator |