![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > 1lt3 | Structured version Unicode version |
Description: 1 is less than 3. (Contributed by NM, 26-Sep-2010.) |
Ref | Expression |
---|---|
1lt3 |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1lt2 10591 |
. 2
![]() ![]() ![]() ![]() | |
2 | 2lt3 10592 |
. 2
![]() ![]() ![]() ![]() | |
3 | 1re 9488 |
. . 3
![]() ![]() ![]() ![]() | |
4 | 2re 10494 |
. . 3
![]() ![]() ![]() ![]() | |
5 | 3re 10498 |
. . 3
![]() ![]() ![]() ![]() | |
6 | 3, 4, 5 | lttri 9603 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 1, 2, 6 | mp2an 672 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: class class
class wbr 4392 ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 ax-sep 4513 ax-nul 4521 ax-pow 4570 ax-pr 4631 ax-un 6474 ax-resscn 9442 ax-1cn 9443 ax-icn 9444 ax-addcl 9445 ax-addrcl 9446 ax-mulcl 9447 ax-mulrcl 9448 ax-mulcom 9449 ax-addass 9450 ax-mulass 9451 ax-distr 9452 ax-i2m1 9453 ax-1ne0 9454 ax-1rid 9455 ax-rnegex 9456 ax-rrecex 9457 ax-cnre 9458 ax-pre-lttri 9459 ax-pre-lttrn 9460 ax-pre-ltadd 9461 ax-pre-mulgt0 9462 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2264 df-mo 2265 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2601 df-ne 2646 df-nel 2647 df-ral 2800 df-rex 2801 df-reu 2802 df-rab 2804 df-v 3072 df-sbc 3287 df-csb 3389 df-dif 3431 df-un 3433 df-in 3435 df-ss 3442 df-nul 3738 df-if 3892 df-pw 3962 df-sn 3978 df-pr 3980 df-op 3984 df-uni 4192 df-br 4393 df-opab 4451 df-mpt 4452 df-id 4736 df-po 4741 df-so 4742 df-xp 4946 df-rel 4947 df-cnv 4948 df-co 4949 df-dm 4950 df-rn 4951 df-res 4952 df-ima 4953 df-iota 5481 df-fun 5520 df-fn 5521 df-f 5522 df-f1 5523 df-fo 5524 df-f1o 5525 df-fv 5526 df-riota 6153 df-ov 6195 df-oprab 6196 df-mpt2 6197 df-er 7203 df-en 7413 df-dom 7414 df-sdom 7415 df-pnf 9523 df-mnf 9524 df-xr 9525 df-ltxr 9526 df-le 9527 df-sub 9700 df-neg 9701 df-2 10483 df-3 10484 |
This theorem is referenced by: 1le3 10641 fztpval 11621 expnass 12074 f1oun2prg 12631 sin01gt0 13578 rpnnen2lem3 13603 rpnnen2lem9 13609 3prm 13884 6nprm 14241 7prm 14242 9nprm 14244 13prm 14247 19prm 14249 prmlem2 14251 37prm 14252 43prm 14253 139prm 14255 163prm 14256 631prm 14258 ressmulr 14395 opprbas 16829 matbas 18425 log2cnv 22457 cxploglim2 22490 dchrvmasumlem2 22865 pntibndlem1 22956 axlowdimlem16 23340 usgraexmpldifpr 23455 3v3e3cycl1 23667 constr3lem4 23670 constr3pthlem1 23678 konigsberg 23745 ex-dif 23767 ex-pss 23772 ex-res 23785 rabren3dioph 29294 jm2.23 29485 stoweidlem34 29969 stoweidlem42 29977 numclwlk1lem2f1 30827 frgraogt3nreg 30853 |
Copyright terms: Public domain | W3C validator |