![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 1lt3 | Structured version Visualization version GIF version |
Description: 1 is less than 3. (Contributed by NM, 26-Sep-2010.) |
Ref | Expression |
---|---|
1lt3 | ⊢ 1 < 3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1lt2 12333 | . 2 ⊢ 1 < 2 | |
2 | 2lt3 12334 | . 2 ⊢ 2 < 3 | |
3 | 1re 11164 | . . 3 ⊢ 1 ∈ ℝ | |
4 | 2re 12236 | . . 3 ⊢ 2 ∈ ℝ | |
5 | 3re 12242 | . . 3 ⊢ 3 ∈ ℝ | |
6 | 3, 4, 5 | lttri 11290 | . 2 ⊢ ((1 < 2 ∧ 2 < 3) → 1 < 3) |
7 | 1, 2, 6 | mp2an 690 | 1 ⊢ 1 < 3 |
Colors of variables: wff setvar class |
Syntax hints: class class class wbr 5110 1c1 11061 < clt 11198 2c2 12217 3c3 12218 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5261 ax-nul 5268 ax-pow 5325 ax-pr 5389 ax-un 7677 ax-resscn 11117 ax-1cn 11118 ax-icn 11119 ax-addcl 11120 ax-addrcl 11121 ax-mulcl 11122 ax-mulrcl 11123 ax-mulcom 11124 ax-addass 11125 ax-mulass 11126 ax-distr 11127 ax-i2m1 11128 ax-1ne0 11129 ax-1rid 11130 ax-rnegex 11131 ax-rrecex 11132 ax-cnre 11133 ax-pre-lttri 11134 ax-pre-lttrn 11135 ax-pre-ltadd 11136 ax-pre-mulgt0 11137 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-reu 3352 df-rab 3406 df-v 3448 df-sbc 3743 df-csb 3859 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4288 df-if 4492 df-pw 4567 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-opab 5173 df-mpt 5194 df-id 5536 df-po 5550 df-so 5551 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-iota 6453 df-fun 6503 df-fn 6504 df-f 6505 df-f1 6506 df-fo 6507 df-f1o 6508 df-fv 6509 df-riota 7318 df-ov 7365 df-oprab 7366 df-mpo 7367 df-er 8655 df-en 8891 df-dom 8892 df-sdom 8893 df-pnf 11200 df-mnf 11201 df-xr 11202 df-ltxr 11203 df-le 11204 df-sub 11396 df-neg 11397 df-2 12225 df-3 12226 |
This theorem is referenced by: 1le3 12374 fztpval 13513 expnass 14122 s4fv1 14797 f1oun2prg 14818 sin01gt0 16083 rpnnen2lem3 16109 rpnnen2lem9 16115 3prm 16581 6nprm 16993 7prm 16994 9nprm 16996 13prm 16999 19prm 17001 prmlem2 17003 37prm 17004 43prm 17005 139prm 17007 163prm 17008 631prm 17010 basendxnmulrndx 17190 basendxnmulrndxOLD 17191 opprbasOLD 20071 log2cnv 26331 cxploglim2 26365 2lgslem3 26789 dchrvmasumlem2 26883 pntibndlem1 26974 tgcgr4 27536 axlowdimlem16 27969 usgrexmpldifpr 28269 upgr3v3e3cycl 29187 upgr4cycl4dv4e 29192 konigsberglem2 29260 konigsberglem3 29261 konigsberglem5 29263 frgrogt3nreg 29404 ex-dif 29430 ex-pss 29435 ex-res 29448 aks4d1p1p3 40599 aks4d1p1p2 40600 aks4d1p1p4 40601 aks4d1p3 40608 acos1half 40695 rabren3dioph 41196 jm2.23 41378 mnringbasedOLD 42614 stoweidlem34 44395 stoweidlem42 44403 smfmullem4 45155 fmtno4prmfac193 45885 3ndvds4 45907 127prm 45911 nnsum4primesodd 46108 nnsum4primesoddALTV 46109 sepfsepc 47080 |
Copyright terms: Public domain | W3C validator |