Theorem 2lt3 12384

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 12285	. . 3 ⊢ 2 ∈ ℝ
2	1	ltp1i 12089	. 2 ⊢ 2 < (2 + 1)
3		df-3 12274	. 2 ⊢ 3 = (2 + 1)
4	2, 3	breqtrri 5124	1 ⊢ 2 < 3

Syntax hints:   class class class wbr 5097  (class class class)co 7390  1c1 11067   + caddc 11069   < clt 11209  2c2 12265  3c3 12266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-resscn 11123  ax-1cn 11124  ax-icn 11125  ax-addcl 11126  ax-addrcl 11127  ax-mulcl 11128  ax-mulrcl 11129  ax-mulcom 11130  ax-addass 11131  ax-mulass 11132  ax-distr 11133  ax-i2m1 11134  ax-1ne0 11135  ax-1rid 11136  ax-rnegex 11137  ax-rrecex 11138  ax-cnre 11139  ax-pre-lttri 11140  ax-pre-lttrn 11141  ax-pre-ltadd 11142  ax-pre-mulgt0 11143

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-reu 3367  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-riota 7347  df-ov 7393  df-oprab 7394  df-mpo 7395  df-er 8671  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11211  df-mnf 11212  df-xr 11213  df-ltxr 11214  df-le 11215  df-sub 11409  df-neg 11410  df-2 12273  df-3 12274

This theorem is referenced by:  2le3  12385  1lt3  12386  2lt4  12388  2lt6  12397  2lt7  12403  2lt8  12410  2lt9  12418  3halfnz  12645  uzuzle23  12878  uz3m2nn  12888  fztpval  13584  fvf1tp  13792  expnass  14214  hash3tpde  14499  tpf1ofv2  14504  tpfo  14506  s4fv2  14903  f1oun2prg  14923  caucvgrlem  15690  cos01gt0  16213  3lcm2e6  16757  5prm  17134  11prm  17141  17prm  17143  23prm  17145  83prm  17149  317prm  17152  4001lem4  17170  plusgndxnmulrndx  17316  rngstr  17317  slotsdifunifndx  17420  cnfldstr  21413  2logb9irr  26847  2logb3irr  26849  log2le1  27002  chtub  27263  bpos1  27334  bposlem6  27340  chto1ub  27527  dchrvmasumiflem1  27552  istrkg3ld  28617  tgcgr4  28687  axlowdimlem2  29100  axlowdimlem16  29114  axlowdimlem17  29115  axlowdim  29118  usgrexmpldifpr  29415  upgr3v3e3cycl  30338  konigsbergiedgw  30406  konigsberglem1  30410  konigsberglem2  30411  konigsberglem3  30412  ex-pss  30586  ex-res  30599  ex-fv  30601  ex-fl  30605  ex-mod  30607  evl1deg3  33734  2sqr3minply  34037  2sqr3nconstr  34038  cos9thpinconstrlem2  34047  prodfzo03  34857  cnndvlem1  36935  poimirlem9  38088  3lexlogpow2ineq1  42635  aks4d1p1p6  42650  aks4d1p1p5  42652  2ap1caineq  42722  rabren3dioph  43352  wallispilem4  46602  fourierdlem87  46727  smfmullem4  47328  257prm  48130  31prm  48166  9fppr8  48319  fpprel2  48323  nnsum3primes4  48370  nnsum3primesgbe  48374  nnsum3primesle9  48376  nnsum4primesodd  48378  nnsum4primesoddALTV  48379  tgoldbach  48399  cycl3grtri  48529  usgrexmpl1lem  48603  usgrexmpl2lem  48608  usgrexmpl2nb2  48615  usgrexmpl2nb3  48616  usgrexmpl2trifr  48619  gpg3nbgrvtx0  48658  gpg3kgrtriexlem1  48665  zlmodzxznm  49079  zlmodzxzldeplem  49080  sepfsepc  49509