Theorem 2lt4 12228

Description: 2 is less than 4. (Contributed by Mario Carneiro, 15-Sep-2013.)

Assertion

Ref	Expression
2lt4	⊢ 2 < 4

Proof of Theorem 2lt4

Step	Hyp	Ref	Expression
1		2lt3 12225	. 2 ⊢ 2 < 3
2		3lt4 12227	. 2 ⊢ 3 < 4
3		2re 12127	. . 3 ⊢ 2 ∈ ℝ
4		3re 12133	. . 3 ⊢ 3 ∈ ℝ
5		4re 12137	. . 3 ⊢ 4 ∈ ℝ
6	3, 4, 5	lttri 11181	. 2 ⊢ ((2 < 3 ∧ 3 < 4) → 2 < 4)
7	1, 2, 6	mp2an 689	1 ⊢ 2 < 4

Syntax hints:   class class class wbr 5087   < clt 11089  2c2 12108  3c3 12109  4c4 12110

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 2708  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028

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 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-br 5088  df-opab 5150  df-mpt 5171  df-id 5507  df-po 5521  df-so 5522  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-er 8548  df-en 8784  df-dom 8785  df-sdom 8786  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-2 12116  df-3 12117  df-4 12118

This theorem is referenced by:  1lt4  12229  2lt5  12232  eluz4eluz2  12705  fz0to4untppr  13439  fzo0to42pr  13554  4bc2eq6  14123  sqrt2gt1lt2  15065  cos01bnd  15974  4sqlem12  16734  starvndxnplusgndx  17092  prdsvalstr  17240  cnfldfunALTOLD  20694  pcoass  24270  pilem3  25695  ppiublem1  26433  bpos1  26514  2sqlem11  26660  2sqreultlem  26678  2sqreunnltlem  26681  usgrexmplef  27762  upgr4cycl4dv4e  28685  sqsscirc1  31998  iccioo01  35570  hlhilsplusOLD  40178  flt4lem7  40712  fmtno4prmfac  45289  sbgoldbalt  45498