MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lttri Unicode version

Theorem lttri 9731
Description: 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
Hypotheses
Ref Expression
lt.1
lt.2
lt.3
Assertion
Ref Expression
lttri

Proof of Theorem lttri
StepHypRef Expression
1 lt.1 . 2
2 lt.2 . 2
3 lt.3 . 2
4 lttr 9682 . 2
51, 2, 3, 4mp3an 1324 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818   class class class wbr 4452   cr 9512   clt 9649
This theorem is referenced by:  1lt3  10729  2lt4  10731  1lt4  10732  3lt5  10734  2lt5  10735  1lt5  10736  4lt6  10738  3lt6  10739  2lt6  10740  1lt6  10741  5lt7  10743  4lt7  10744  3lt7  10745  2lt7  10746  1lt7  10747  6lt8  10749  5lt8  10750  4lt8  10751  3lt8  10752  2lt8  10753  1lt8  10754  7lt9  10756  6lt9  10757  5lt9  10758  4lt9  10759  3lt9  10760  2lt9  10761  1lt9  10762  8lt10  10764  7lt10  10765  6lt10  10766  5lt10  10767  4lt10  10768  3lt10  10769  2lt10  10770  1lt10  10771  sincos2sgn  13929  epos  13940  dvdslelem  14030  oppcbas  15113  sralem  17823  zlmlem  18554  psgnodpmr  18626  tnglem  21154  xrhmph  21447  vitalilem4  22020  pipos  22853  logneg  22972  asin1  23225  reasinsin  23227  atan1  23259  bposlem8  23566  bposlem9  23567  chebbnd1lem2  23655  chebbnd1lem3  23656  chebbnd1  23657  mulog2sumlem2  23720  pntibndlem1  23774  pntlemb  23782  pntlemk  23791  ttglem  24179  cchhllem  24190  axlowdimlem16  24260  log2le1  28023  sgnnbi  28484  sgnpbi  28485  signswch  28518  logi  29121  asindmre  30102  fdc  30238  fourierdlem94  31983  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fourierdlem113  32002  fourierdlem114  32003  fouriersw  32014  etransclem23  32040  ene1  33168  bj-minftyccb  34628  bj-pinftynminfty  34630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-resscn 9570  ax-pre-lttrn 9588
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-er 7330  df-en 7537  df-dom 7538  df-sdom 7539  df-pnf 9651  df-mnf 9652  df-ltxr 9654
  Copyright terms: Public domain W3C validator