Theorem 2lt3 12314

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

Assertion

Ref	Expression
2lt3	⊢ 2 < 3

Proof of Theorem 2lt3

Step	Hyp	Ref	Expression
1		2re 12221	. . 3 ⊢ 2 ∈ ℝ
2	1	ltp1i 12048	. 2 ⊢ 2 < (2 + 1)
3		df-3 12211	. 2 ⊢ 3 = (2 + 1)
4	2, 3	breqtrri 5122	1 ⊢ 2 < 3

Syntax hints:   class class class wbr 5095  (class class class)co 7353  1c1 11029   + caddc 11031   < clt 11168  2c2 12202  3c3 12203

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7675  ax-resscn 11085  ax-1cn 11086  ax-icn 11087  ax-addcl 11088  ax-addrcl 11089  ax-mulcl 11090  ax-mulrcl 11091  ax-mulcom 11092  ax-addass 11093  ax-mulass 11094  ax-distr 11095  ax-i2m1 11096  ax-1ne0 11097  ax-1rid 11098  ax-rnegex 11099  ax-rrecex 11100  ax-cnre 11101  ax-pre-lttri 11102  ax-pre-lttrn 11103  ax-pre-ltadd 11104  ax-pre-mulgt0 11105

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-reu 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-po 5531  df-so 5532  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7310  df-ov 7356  df-oprab 7357  df-mpo 7358  df-er 8632  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174  df-sub 11368  df-neg 11369  df-2 12210  df-3 12211

This theorem is referenced by:  1lt3  12315  2lt4  12317  2lt6  12326  2lt7  12332  2lt8  12339  2lt9  12347  3halfnz  12574  2lt10  12748  uzuzle23  12804  uz3m2nn  12814  fztpval  13508  fvf1tp  13712  expnass  14134  hash3tpde  14419  tpf1ofv2  14424  tpfo  14426  s4fv2  14823  f1oun2prg  14843  caucvgrlem  15599  cos01gt0  16119  3lcm2e6  16662  5prm  17039  11prm  17045  17prm  17047  23prm  17049  83prm  17053  317prm  17056  4001lem4  17074  plusgndxnmulrndx  17220  rngstr  17221  slotsdifunifndx  17324  cnfldstr  21282  cnfldstrOLD  21297  2logb9irr  26722  2logb3irr  26724  log2le1  26877  chtub  27140  bpos1  27211  bposlem6  27217  chto1ub  27404  dchrvmasumiflem1  27429  istrkg3ld  28425  tgcgr4  28495  axlowdimlem2  28907  axlowdimlem16  28921  axlowdimlem17  28922  axlowdim  28925  usgrexmpldifpr  29222  upgr3v3e3cycl  30143  konigsbergiedgw  30211  konigsberglem1  30215  konigsberglem2  30216  konigsberglem3  30217  ex-pss  30391  ex-res  30404  ex-fv  30406  ex-fl  30410  ex-mod  30412  evl1deg3  33532  2sqr3minply  33766  2sqr3nconstr  33767  cos9thpinconstrlem2  33776  prodfzo03  34590  cnndvlem1  36530  poimirlem9  37628  3lexlogpow2ineq1  42051  aks4d1p1p6  42066  aks4d1p1p5  42068  2ap1caineq  42138  rabren3dioph  42808  jm2.20nn  42990  wallispilem4  46069  fourierdlem87  46194  smfmullem4  46795  257prm  47565  31prm  47601  9fppr8  47741  fpprel2  47745  nnsum3primes4  47792  nnsum3primesgbe  47796  nnsum3primesle9  47798  nnsum4primesodd  47800  nnsum4primesoddALTV  47801  tgoldbach  47821  cycl3grtri  47951  usgrexmpl1lem  48025  usgrexmpl2lem  48030  usgrexmpl2nb2  48037  usgrexmpl2nb3  48038  usgrexmpl2trifr  48041  gpg3nbgrvtx0  48080  gpg3kgrtriexlem1  48087  zlmodzxznm  48502  zlmodzxzldeplem  48503  sepfsepc  48932