Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > lelttrd | Unicode version |
Description: Transitive law deduction for 'less than or equal to', 'less than'. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
ltd.1 | |
ltd.2 | |
letrd.3 | |
lelttrd.4 | |
lelttrd.5 |
Ref | Expression |
---|---|
lelttrd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lelttrd.4 | . 2 | |
2 | lelttrd.5 | . 2 | |
3 | ltd.1 | . . 3 | |
4 | ltd.2 | . . 3 | |
5 | letrd.3 | . . 3 | |
6 | lelttr 8001 | . . 3 | |
7 | 3, 4, 5, 6 | syl3anc 1233 | . 2 |
8 | 1, 2, 7 | mp2and 431 | 1 |
Copyright terms: Public domain | W3C validator |