Theorem 2lt3 12224

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 12126	. . 3 ⊢ 2 ∈ ℝ
2	1	ltp1i 11958	. 2 ⊢ 2 < (2 + 1)
3		df-3 12116	. 2 ⊢ 3 = (2 + 1)
4	2, 3	breqtrri 5113	1 ⊢ 2 < 3

Syntax hints:   class class class wbr 5086  (class class class)co 7316  1c1 10951   + caddc 10953   < clt 11088  2c2 12107  3c3 12108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5237  ax-nul 5244  ax-pow 5302  ax-pr 5366  ax-un 7629  ax-resscn 11007  ax-1cn 11008  ax-icn 11009  ax-addcl 11010  ax-addrcl 11011  ax-mulcl 11012  ax-mulrcl 11013  ax-mulcom 11014  ax-addass 11015  ax-mulass 11016  ax-distr 11017  ax-i2m1 11018  ax-1ne0 11019  ax-1rid 11020  ax-rnegex 11021  ax-rrecex 11022  ax-cnre 11023  ax-pre-lttri 11024  ax-pre-lttrn 11025  ax-pre-ltadd 11026  ax-pre-mulgt0 11027

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3350  df-rab 3404  df-v 3442  df-sbc 3726  df-csb 3842  df-dif 3899  df-un 3901  df-in 3903  df-ss 3913  df-nul 4267  df-if 4471  df-pw 4546  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4850  df-br 5087  df-opab 5149  df-mpt 5170  df-id 5506  df-po 5520  df-so 5521  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-riota 7273  df-ov 7319  df-oprab 7320  df-mpo 7321  df-er 8547  df-en 8783  df-dom 8784  df-sdom 8785  df-pnf 11090  df-mnf 11091  df-xr 11092  df-ltxr 11093  df-le 11094  df-sub 11286  df-neg 11287  df-2 12115  df-3 12116

This theorem is referenced by:  1lt3  12225  2lt4  12227  2lt6  12236  2lt7  12242  2lt8  12249  2lt9  12257  3halfnz  12478  2lt10  12654  uzuzle23  12708  uz3m2nn  12710  fztpval  13397  expnass  14003  s4fv2  14686  f1oun2prg  14706  caucvgrlem  15460  cos01gt0  15976  3lcm2e6  16510  5prm  16884  11prm  16890  17prm  16892  23prm  16894  83prm  16898  317prm  16901  4001lem4  16919  plusgndxnmulrndx  17081  rngstr  17082  slotsdifunifndx  17185  oppraddOLD  19944  cnfldstr  20679  cnfldfunALTOLD  20691  2logb9irr  26025  2logb3irr  26027  log2le1  26180  chtub  26440  bpos1  26511  bposlem6  26517  chto1ub  26704  dchrvmasumiflem1  26729  istrkg3ld  26955  tgcgr4  27025  axlowdimlem2  27444  axlowdimlem16  27458  axlowdimlem17  27459  axlowdim  27462  usgrexmpldifpr  27758  upgr3v3e3cycl  28676  konigsbergiedgw  28744  konigsberglem1  28748  konigsberglem2  28749  konigsberglem3  28750  ex-pss  28924  ex-res  28937  ex-fv  28939  ex-fl  28943  ex-mod  28945  prodfzo03  32719  cnndvlem1  34787  poimirlem9  35863  3lexlogpow2ineq1  40292  aks4d1p1p6  40307  aks4d1p1p5  40309  2ap1caineq  40330  rabren3dioph  40858  jm2.20nn  41041  mnringaddgdOLD  42075  wallispilem4  43864  fourierdlem87  43989  smfmullem4  44588  257prm  45283  31prm  45319  9fppr8  45459  fpprel2  45463  nnsum3primes4  45510  nnsum3primesgbe  45514  nnsum3primesle9  45516  nnsum4primesodd  45518  nnsum4primesoddALTV  45519  tgoldbach  45539  zlmodzxznm  46108  zlmodzxzldeplem  46109  sepfsepc  46491