Theorem 1lt3 12357

Description: 1 is less than 3. (Contributed by NM, 26-Sep-2010.)

Assertion

Ref	Expression
1lt3	⊢ 1 < 3

Proof of Theorem 1lt3

Step	Hyp	Ref	Expression
1		1lt2 12355	. 2 ⊢ 1 < 2
2		2lt3 12356	. 2 ⊢ 2 < 3
3		1re 11186	. . 3 ⊢ 1 ∈ ℝ
4		2re 12258	. . 3 ⊢ 2 ∈ ℝ
5		3re 12264	. . 3 ⊢ 3 ∈ ℝ
6	3, 4, 5	lttri 11312	. 2 ⊢ ((1 < 2 ∧ 2 < 3) → 1 < 3)
7	1, 2, 6	mp2an 690	1 ⊢ 1 < 3

Syntax hints:   class class class wbr 5132  1c1 11083   < clt 11220  2c2 12239  3c3 12240

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 5283  ax-nul 5290  ax-pow 5347  ax-pr 5411  ax-un 7699  ax-resscn 11139  ax-1cn 11140  ax-icn 11141  ax-addcl 11142  ax-addrcl 11143  ax-mulcl 11144  ax-mulrcl 11145  ax-mulcom 11146  ax-addass 11147  ax-mulass 11148  ax-distr 11149  ax-i2m1 11150  ax-1ne0 11151  ax-1rid 11152  ax-rnegex 11153  ax-rrecex 11154  ax-cnre 11155  ax-pre-lttri 11156  ax-pre-lttrn 11157  ax-pre-ltadd 11158  ax-pre-mulgt0 11159

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 3372  df-rab 3426  df-v 3468  df-sbc 3765  df-csb 3881  df-dif 3938  df-un 3940  df-in 3942  df-ss 3952  df-nul 4310  df-if 4514  df-pw 4589  df-sn 4614  df-pr 4616  df-op 4620  df-uni 4893  df-br 5133  df-opab 5195  df-mpt 5216  df-id 5558  df-po 5572  df-so 5573  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6475  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-riota 7340  df-ov 7387  df-oprab 7388  df-mpo 7389  df-er 8677  df-en 8913  df-dom 8914  df-sdom 8915  df-pnf 11222  df-mnf 11223  df-xr 11224  df-ltxr 11225  df-le 11226  df-sub 11418  df-neg 11419  df-2 12247  df-3 12248

This theorem is referenced by:  1le3  12396  fztpval  13535  expnass  14144  s4fv1  14819  f1oun2prg  14840  sin01gt0  16105  rpnnen2lem3  16131  rpnnen2lem9  16137  3prm  16603  6nprm  17015  7prm  17016  9nprm  17018  13prm  17021  19prm  17023  prmlem2  17025  37prm  17026  43prm  17027  139prm  17029  163prm  17030  631prm  17032  basendxnmulrndx  17212  basendxnmulrndxOLD  17213  opprbasOLD  20093  log2cnv  26353  cxploglim2  26387  2lgslem3  26811  dchrvmasumlem2  26905  pntibndlem1  26996  tgcgr4  27577  axlowdimlem16  28010  usgrexmpldifpr  28310  upgr3v3e3cycl  29228  upgr4cycl4dv4e  29233  konigsberglem2  29301  konigsberglem3  29302  konigsberglem5  29304  frgrogt3nreg  29445  ex-dif  29471  ex-pss  29476  ex-res  29489  aks4d1p1p3  40639  aks4d1p1p2  40640  aks4d1p1p4  40641  aks4d1p3  40648  acos1half  40735  rabren3dioph  41236  jm2.23  41418  mnringbasedOLD  42654  stoweidlem34  44435  stoweidlem42  44443  smfmullem4  45195  fmtno4prmfac193  45925  3ndvds4  45947  127prm  45951  nnsum4primesodd  46148  nnsum4primesoddALTV  46149  sepfsepc  47120