| Intuitionistic Logic Explorer | 
      
      
      < Previous  
      Next >
      
       Nearby theorems  | 
  ||
| Mirrors > Home > ILE Home > Th. List > ltled | Unicode version | ||
| Description: 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) | 
| Ref | Expression | 
|---|---|
| ltd.1 | 
 | 
| ltd.2 | 
 | 
| ltled.1 | 
 | 
| Ref | Expression | 
|---|---|
| ltled | 
 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | ltled.1 | 
. 2
 | |
| 2 | ltd.1 | 
. . 3
 | |
| 3 | ltd.2 | 
. . 3
 | |
| 4 | ltle 8114 | 
. . 3
 | |
| 5 | 2, 3, 4 | syl2anc 411 | 
. 2
 | 
| 6 | 1, 5 | mpd 13 | 
1
 | 
| Copyright terms: Public domain | W3C validator |