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

Theorem lttrd 11317
Description: Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.)
Hypotheses
Ref Expression
ltd.1 (𝜑𝐴 ∈ ℝ)
ltd.2 (𝜑𝐵 ∈ ℝ)
letrd.3 (𝜑𝐶 ∈ ℝ)
lttrd.4 (𝜑𝐴 < 𝐵)
lttrd.5 (𝜑𝐵 < 𝐶)
Assertion
Ref Expression
lttrd (𝜑𝐴 < 𝐶)

Proof of Theorem lttrd
StepHypRef Expression
1 lttrd.4 . 2 (𝜑𝐴 < 𝐵)
2 lttrd.5 . 2 (𝜑𝐵 < 𝐶)
3 ltd.1 . . 3 (𝜑𝐴 ∈ ℝ)
4 ltd.2 . . 3 (𝜑𝐵 ∈ ℝ)
5 letrd.3 . . 3 (𝜑𝐶 ∈ ℝ)
6 lttr 11232 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
73, 4, 5, 6syl3anc 1372 . 2 (𝜑 → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
81, 2, 7mp2and 698 1 (𝜑𝐴 < 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wcel 2107   class class class wbr 5106  cr 11051   < clt 11190
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673  ax-resscn 11109  ax-pre-lttrn 11127
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-nel 3051  df-ral 3066  df-rex 3075  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-er 8649  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11192  df-mnf 11193  df-ltxr 11195
This theorem is referenced by:  nnne0  12188  expgt1  14007  ltexp2a  14072  expcan  14075  ltexp2  14076  leexp2  14077  expnlbnd2  14138  expmulnbnd  14139  reccn2  15480  efgt1  15999  tanhlt1  16043  ruclem2  16115  isprm7  16585  pythagtriplem13  16700  fldivp1  16770  4sqlem12  16829  sylow1lem1  19381  telgsums  19771  chfacffsupp  22208  chfacfscmul0  22210  chfacfpmmul0  22214  nrginvrcnlem  24058  iccntr  24187  icccmplem2  24189  opnreen  24197  pjthlem1  24804  pmltpclem2  24816  ovollb2lem  24855  opnmbllem  24968  volivth  24974  lhop1lem  25380  dvcnvrelem1  25384  dvcvx  25387  ftc1lem4  25406  aaliou3lem7  25712  ulmdvlem1  25762  reeff1olem  25808  pilem2  25814  pilem3  25815  tangtx  25865  tanord1  25896  tanord  25897  rplogcl  25962  logimul  25972  logcnlem3  26002  efopnlem1  26014  cxplt  26052  cxple  26053  cxpcn3lem  26103  asinsin  26245  atanlogaddlem  26266  atanlogsublem  26268  cxp2limlem  26328  cxp2lim  26329  zetacvg  26367  lgamucov  26390  lgamcvg2  26407  ftalem1  26425  mersenne  26578  bposlem2  26636  bposlem6  26640  bposlem9  26643  lgsqrlem2  26698  lgsquadlem2  26732  chebbnd1lem2  26821  chebbnd1lem3  26822  chebbnd1  26823  chtppilimlem1  26824  chto1ub  26827  mulog2sumlem2  26886  chpdifbndlem1  26904  selberg3lem1  26908  pntrlog2bndlem2  26929  pntrlog2bndlem4  26931  pntpbnd1a  26936  pntpbnd1  26937  pntpbnd2  26938  pntibndlem1  26940  pntibndlem2  26942  pntibndlem3  26943  pntibnd  26944  pntlemb  26948  pntlemr  26953  pntlemf  26956  pnt  26965  ostth2lem1  26969  ostth2lem3  26986  ostth2lem4  26987  wwlksext2clwwlk  29004  frgrogt3nreg  29344  friendshipgt3  29345  pjhthlem1  30336  psgnfzto1stlem  31952  1smat1  32388  sqsscirc1  32492  xrge0iifiso  32519  sgnsub  33147  signslema  33177  chtvalz  33245  hgt750lemd  33264  knoppndvlem12  34989  knoppndvlem14  34991  knoppndvlem15  34992  knoppndvlem17  34994  knoppndvlem20  34997  poimirlem6  36087  poimirlem7  36088  poimirlem8  36089  poimirlem15  36096  poimirlem20  36101  poimirlem28  36109  opnmbllem0  36117  itg2gt0cn  36136  ftc1cnnclem  36152  ftc1anc  36162  cntotbnd  36258  3lexlogpow5ineq3  40517  3lexlogpow2ineq2  40519  3lexlogpow5ineq5  40520  aks4d1lem1  40522  0nonelalab  40527  aks4d1p1p3  40529  aks4d1p1p2  40530  aks4d1p1p4  40531  aks4d1p1p6  40533  aks4d1p1p7  40534  aks4d1p1p5  40535  aks4d1p1  40536  aks4d1p2  40537  aks4d1p3  40538  aks4d1p6  40541  aks4d1p7d1  40542  aks4d1p7  40543  aks4d1p8d3  40546  aks4d1p8  40547  2ap1caineq  40556  sticksstones1  40557  sn-addlt0d  40918  sn-addgt0d  40919  flt4lem7  41000  fltnlta  41004  pellexlem5  41159  pellfundex  41212  pellfundrp  41214  rmspecfund  41235  monotuz  41268  jm3.1lem2  41345  jm3.1lem3  41346  imo72b2  42452  prmunb2  42598  neglt  43525  ltadd12dd  43584  infleinflem2  43612  sqrlearg  43798  lptre2pt  43888  0ellimcdiv  43897  limsup10exlem  44020  ioodvbdlimc1lem1  44179  iblspltprt  44221  itgspltprt  44227  stoweidlem7  44255  stoweidlem11  44259  stoweidlem13  44261  stoweidlem14  44262  stoweidlem26  44274  stoweidlem42  44290  stoweidlem52  44300  stoweidlem59  44307  stoweidlem60  44308  stoweidlem62  44310  wallispilem4  44316  wallispi  44318  stirlinglem1  44322  stirlinglem3  44324  stirlinglem6  44327  stirlinglem7  44328  stirlinglem10  44331  stirlinglem11  44332  dirkercncflem1  44351  dirkercncflem2  44352  fourierdlem10  44365  fourierdlem11  44366  fourierdlem12  44367  fourierdlem42  44397  fourierdlem47  44401  fourierdlem50  44404  fourierdlem51  44405  fourierdlem73  44427  fourierdlem79  44433  fourierdlem83  44437  fourierdlem103  44457  fourierdlem104  44458  sqwvfoura  44476  sqwvfourb  44477  fouriersw  44479  hoidmvlelem1  44843  hoiqssbllem2  44871  hspmbllem1  44874  pimrecltpos  44956  pimrecltneg  44972  smfaddlem1  45011  smflimlem3  45021  smflimlem4  45022  smfmullem1  45039  fpprel2  45940  eenglngeehlnmlem2  46831
  Copyright terms: Public domain W3C validator