Theorem 2lt3 12381

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 12282	. . 3 ⊢ 2 ∈ ℝ
2	1	ltp1i 12086	. 2 ⊢ 2 < (2 + 1)
3		df-3 12271	. 2 ⊢ 3 = (2 + 1)
4	2, 3	breqtrri 5121	1 ⊢ 2 < 3

Syntax hints:   class class class wbr 5094  (class class class)co 7385  1c1 11064   + caddc 11066   < clt 11206  2c2 12262  3c3 12263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1809  ax-4 1823  ax-5 1924  ax-6 1981  ax-7 2022  ax-8 2138  ax-9 2146  ax-10 2169  ax-11 2185  ax-12 2206  ax-ext 2728  ax-sep 5240  ax-nul 5250  ax-pow 5316  ax-pr 5384  ax-un 7707  ax-resscn 11120  ax-1cn 11121  ax-icn 11122  ax-addcl 11123  ax-addrcl 11124  ax-mulcl 11125  ax-mulrcl 11126  ax-mulcom 11127  ax-addass 11128  ax-mulass 11129  ax-distr 11130  ax-i2m1 11131  ax-1ne0 11132  ax-1rid 11133  ax-rnegex 11134  ax-rrecex 11135  ax-cnre 11136  ax-pre-lttri 11137  ax-pre-lttrn 11138  ax-pre-ltadd 11139  ax-pre-mulgt0 11140

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1557  df-fal 1567  df-ex 1794  df-nf 1798  df-sb 2085  df-mo 2560  df-eu 2590  df-clab 2735  df-cleq 2748  df-clel 2831  df-nfc 2905  df-ne 2952  df-nel 3056  df-ral 3071  df-rex 3081  df-reu 3362  df-rab 3409  df-v 3450  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4475  df-pw 4551  df-sn 4577  df-pr 4579  df-op 4583  df-uni 4860  df-br 5095  df-opab 5157  df-mpt 5176  df-id 5535  df-po 5548  df-so 5549  df-xp 5646  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-res 5652  df-ima 5653  df-iota 6466  df-fun 6512  df-fn 6513  df-f 6514  df-f1 6515  df-fo 6516  df-f1o 6517  df-fv 6518  df-riota 7342  df-ov 7388  df-oprab 7389  df-mpo 7390  df-er 8666  df-en 8917  df-dom 8918  df-sdom 8919  df-pnf 11208  df-mnf 11209  df-xr 11210  df-ltxr 11211  df-le 11212  df-sub 11406  df-neg 11407  df-2 12270  df-3 12271

This theorem is referenced by:  2le3  12382  1lt3  12383  2lt4  12385  2lt6  12394  2lt7  12400  2lt8  12407  2lt9  12415  3halfnz  12642  uzuzle23  12875  uz3m2nn  12885  fztpval  13581  fvf1tp  13789  expnass  14211  hash3tpde  14496  tpf1ofv2  14501  tpfo  14503  s4fv2  14900  f1oun2prg  14920  caucvgrlem  15676  cos01gt0  16199  3lcm2e6  16743  5prm  17120  11prm  17127  17prm  17129  23prm  17131  83prm  17135  317prm  17138  4001lem4  17156  plusgndxnmulrndx  17302  rngstr  17303  slotsdifunifndx  17406  cnfldstr  21399  2logb9irr  26830  2logb3irr  26832  log2le1  26985  chtub  27246  bpos1  27317  bposlem6  27323  chto1ub  27510  dchrvmasumiflem1  27535  istrkg3ld  28600  tgcgr4  28670  axlowdimlem2  29083  axlowdimlem16  29097  axlowdimlem17  29098  axlowdim  29101  usgrexmpldifpr  29398  upgr3v3e3cycl  30321  konigsbergiedgw  30389  konigsberglem1  30393  konigsberglem2  30394  konigsberglem3  30395  ex-pss  30569  ex-res  30582  ex-fv  30584  ex-fl  30588  ex-mod  30590  evl1deg3  33728  2sqr3minply  34031  2sqr3nconstr  34032  cos9thpinconstrlem2  34041  prodfzo03  34854  cnndvlem1  36923  poimirlem9  38076  3lexlogpow2ineq1  42623  aks4d1p1p6  42638  aks4d1p1p5  42640  2ap1caineq  42710  rabren3dioph  43340  wallispilem4  46590  fourierdlem87  46715  smfmullem4  47316  257prm  48118  31prm  48154  9fppr8  48307  fpprel2  48311  nnsum3primes4  48358  nnsum3primesgbe  48362  nnsum3primesle9  48364  nnsum4primesodd  48366  nnsum4primesoddALTV  48367  tgoldbach  48387  cycl3grtri  48517  usgrexmpl1lem  48591  usgrexmpl2lem  48596  usgrexmpl2nb2  48603  usgrexmpl2nb3  48604  usgrexmpl2trifr  48607  gpg3nbgrvtx0  48646  gpg3kgrtriexlem1  48653  zlmodzxznm  49067  zlmodzxzldeplem  49068  sepfsepc  49497