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

Theorem lttrd 9195
Description: Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.)
Hypotheses
Ref Expression
ltd.1  |-  ( ph  ->  A  e.  RR )
ltd.2  |-  ( ph  ->  B  e.  RR )
letrd.3  |-  ( ph  ->  C  e.  RR )
lttrd.4  |-  ( ph  ->  A  <  B )
lttrd.5  |-  ( ph  ->  B  <  C )
Assertion
Ref Expression
lttrd  |-  ( ph  ->  A  <  C )

Proof of Theorem lttrd
StepHypRef Expression
1 lttrd.4 . 2  |-  ( ph  ->  A  <  B )
2 lttrd.5 . 2  |-  ( ph  ->  B  <  C )
3 ltd.1 . . 3  |-  ( ph  ->  A  e.  RR )
4 ltd.2 . . 3  |-  ( ph  ->  B  e.  RR )
5 letrd.3 . . 3  |-  ( ph  ->  C  e.  RR )
6 lttr 9116 . . 3  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <  B  /\  B  <  C )  ->  A  <  C
) )
73, 4, 5, 6syl3anc 1184 . 2  |-  ( ph  ->  ( ( A  < 
B  /\  B  <  C )  ->  A  <  C ) )
81, 2, 7mp2and 661 1  |-  ( ph  ->  A  <  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   class class class wbr 4180   RRcr 8953    < clt 9084
This theorem is referenced by:  expgt1  11381  ltexp2a  11394  expcan  11395  ltexp2  11396  leexp2  11397  expnlbnd2  11473  expmulnbnd  11474  reccn2  12353  efgt1  12680  tanhlt1  12724  ruclem2  12794  pythagtriplem13  13164  fldivp1  13229  4sqlem12  13287  sylow1lem1  15195  nrginvrcnlem  18687  iccntr  18813  icccmplem2  18815  opnreen  18823  pjthlem1  19299  pmltpclem2  19307  ovollb2lem  19345  opnmbllem  19454  volivth  19460  lhop1lem  19858  dvcnvrelem1  19862  dvcvx  19865  ftc1lem4  19884  aaliou3lem7  20227  ulmdvlem1  20277  reeff1olem  20323  pilem2  20329  pilem3  20330  tangtx  20374  tanord1  20400  tanord  20401  rplogcl  20460  logimul  20470  logcnlem3  20496  efopnlem1  20508  cxplt  20546  cxple  20547  cxpcn3lem  20592  asinsin  20693  atanlogaddlem  20714  atanlogsublem  20716  cxp2limlem  20775  cxp2lim  20776  ftalem1  20816  mersenne  20972  bposlem2  21030  bposlem6  21034  bposlem9  21037  lgsqrlem2  21087  lgsquadlem2  21100  chebbnd1lem2  21125  chebbnd1lem3  21126  chebbnd1  21127  chtppilimlem1  21128  chto1ub  21131  mulog2sumlem2  21190  chpdifbndlem1  21208  selberg3lem1  21212  pntrlog2bndlem2  21233  pntrlog2bndlem4  21235  pntpbnd1a  21240  pntpbnd1  21241  pntpbnd2  21242  pntibndlem1  21244  pntibndlem2  21246  pntibndlem3  21247  pntibnd  21248  pntlemb  21252  pntlemr  21257  pntlemf  21260  pnt  21269  ostth2lem1  21273  ostth2lem3  21290  ostth2lem4  21291  eupap1  21659  pjhthlem1  22854  sqsscirc1  24267  xrge0iifiso  24282  zetacvg  24760  lgamucov  24783  lgamcvg2  24800  mblfinlem  26151  itg2gt0cn  26167  ftc1cnnclem  26185  cntotbnd  26403  pellexlem5  26794  pellfundex  26847  pellfundrp  26849  rmspecfund  26870  monotuz  26902  jm3.1lem2  26987  jm3.1lem3  26988  stoweidlem7  27631  stoweidlem11  27635  stoweidlem13  27637  stoweidlem14  27638  stoweidlem26  27650  stoweidlem42  27666  stoweidlem52  27676  stoweidlem59  27683  stoweidlem60  27684  stoweidlem62  27686  wallispilem4  27692  wallispi  27694  stirlinglem1  27698  stirlinglem3  27700  stirlinglem6  27703  stirlinglem7  27704  stirlinglem10  27707  stirlinglem11  27708
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-resscn 9011  ax-pre-lttrn 9029
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-nel 2578  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-mpt 4236  df-id 4466  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-er 6872  df-en 7077  df-dom 7078  df-sdom 7079  df-pnf 9086  df-mnf 9087  df-ltxr 9089
  Copyright terms: Public domain W3C validator