Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ltleii | Unicode version |
Description: 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.) |
Ref | Expression |
---|---|
lt.1 | |
lt.2 | |
ltlei.1 |
Ref | Expression |
---|---|
ltleii |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltlei.1 | . 2 | |
2 | lt.1 | . . 3 | |
3 | lt.2 | . . 3 | |
4 | 2, 3 | ltlei 7982 | . 2 |
5 | 1, 4 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 2128 class class class wbr 3967 cr 7734 clt 7915 cle 7916 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-13 2130 ax-14 2131 ax-ext 2139 ax-sep 4085 ax-pow 4138 ax-pr 4172 ax-un 4396 ax-setind 4499 ax-cnex 7826 ax-resscn 7827 ax-pre-ltirr 7847 ax-pre-lttrn 7849 |
This theorem depends on definitions: df-bi 116 df-3an 965 df-tru 1338 df-fal 1341 df-nf 1441 df-sb 1743 df-eu 2009 df-mo 2010 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ne 2328 df-nel 2423 df-ral 2440 df-rex 2441 df-rab 2444 df-v 2714 df-dif 3104 df-un 3106 df-in 3108 df-ss 3115 df-pw 3546 df-sn 3567 df-pr 3568 df-op 3570 df-uni 3775 df-br 3968 df-opab 4029 df-xp 4595 df-cnv 4597 df-pnf 7917 df-mnf 7918 df-xr 7919 df-ltxr 7920 df-le 7921 |
This theorem is referenced by: 0le1 8361 1le2 9047 1le3 9050 halfge0 9055 decleh 9335 eluz4eluz2 9484 uzuzle23 9488 fz0to4untppr 10033 fzo0to42pr 10129 4bc2eq6 10660 resqrexlemga 10935 sqrt9 10960 sqrt2gt1lt2 10961 sqrtpclii 11042 0.999... 11430 ef01bndlem 11665 sin01bnd 11666 cos01bnd 11667 cos2bnd 11669 cos12dec 11676 flodddiv4 11838 strleun 12375 dveflem 13183 sinhalfpilem 13208 sincosq1lem 13242 sincos4thpi 13257 sincos6thpi 13259 pigt3 13261 pige3 13262 cosq34lt1 13267 cos02pilt1 13268 cos0pilt1 13269 rpabscxpbnd 13355 2logb9irr 13385 2logb9irrap 13391 ex-fl 13398 ex-gcd 13404 |
Copyright terms: Public domain | W3C validator |