Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > leadd1dd | Structured version Visualization version Unicode version |
Description: Addition to both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 30-May-2016.) |
Ref | Expression |
---|---|
leidd.1 | |
ltnegd.2 | |
ltadd1d.3 | |
leadd1dd.4 |
Ref | Expression |
---|---|
leadd1dd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | leadd1dd.4 | . 2 | |
2 | leidd.1 | . . 3 | |
3 | ltnegd.2 | . . 3 | |
4 | ltadd1d.3 | . . 3 | |
5 | 2, 3, 4 | leadd1d 10621 | . 2 |
6 | 1, 5 | mpbid 222 | 1 |
Copyright terms: Public domain | W3C validator |