![]() |
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 9001 |
. 2
![]() ![]() | |
2 | c1 7843 |
. . 3
![]() ![]() | |
3 | caddc 7845 |
. . 3
![]() ![]() | |
4 | 2, 2, 3 | co 5897 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | wceq 1364 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: 2re 9020 0le2 9040 2pos 9041 1p1e2 9067 2p2e4 9077 2times 9078 3p2e5 9091 4p2e6 9093 5p2e7 9096 6p2e8 9099 7p2e9 9101 2nn 9111 1lt2 9119 nneoor 9386 6p6e12 9488 7p5e12 9491 8p2e10 9494 8p4e12 9496 9p2e11 9501 9p3e12 9502 5t2e10 9514 eluz2b1 9633 nn01to3 9649 fztp 10110 fzprval 10114 fztpval 10115 fzo12sn 10249 rebtwn2zlemstep 10285 rebtwn2z 10287 sqval 10612 fac2 10746 bcp1m1 10780 hashprg 10823 binom11 11529 ege2le3 11714 ef4p 11737 efgt1p2 11738 eirraplem 11819 odd2np1lem 11912 opoe 11935 ncoprmgcdne1b 12124 isprm3 12153 prmind2 12155 dvdsnprmd 12160 prmgt1 12167 pockthlem 12391 pockthg 12392 prmunb 12397 4sqlem19 12444 gsumpr12val 12878 mulg2 13088 dveflem 14664 coskpi 14746 lgslem1 14879 lgsval2lem 14889 lgsdir2lem2 14908 lgsdir2lem3 14909 lgsdirprm 14913 m1lgs 14930 ex-fl 14955 |
Copyright terms: Public domain | W3C validator |