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

Theorem lttrd 10236
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 10152 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
73, 4, 5, 6syl3anc 1366 . 2 (𝜑 → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
81, 2, 7mp2and 715 1 (𝜑𝐴 < 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030   class class class wbr 4685  cr 9973   < clt 10112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-resscn 10031  ax-pre-lttrn 10049
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-pnf 10114  df-mnf 10115  df-ltxr 10117
This theorem is referenced by:  expgt1  12938  ltexp2a  12952  expcan  12953  ltexp2  12954  leexp2  12955  expnlbnd2  13035  expmulnbnd  13036  reccn2  14371  efgt1  14890  tanhlt1  14934  ruclem2  15005  isprm7  15467  pythagtriplem13  15579  fldivp1  15648  4sqlem12  15707  sylow1lem1  18059  telgsums  18436  chfacffsupp  20709  chfacfscmul0  20711  chfacfpmmul0  20715  nrginvrcnlem  22542  iccntr  22671  icccmplem2  22673  opnreen  22681  pjthlem1  23254  pmltpclem2  23264  ovollb2lem  23302  opnmbllem  23415  volivth  23421  lhop1lem  23821  dvcnvrelem1  23825  dvcvx  23828  ftc1lem4  23847  aaliou3lem7  24149  ulmdvlem1  24199  reeff1olem  24245  pilem2  24251  pilem3  24252  tangtx  24302  tanord1  24328  tanord  24329  rplogcl  24395  logimul  24405  logcnlem3  24435  efopnlem1  24447  cxplt  24485  cxple  24486  cxpcn3lem  24533  asinsin  24664  atanlogaddlem  24685  atanlogsublem  24687  cxp2limlem  24747  cxp2lim  24748  zetacvg  24786  lgamucov  24809  lgamcvg2  24826  ftalem1  24844  mersenne  24997  bposlem2  25055  bposlem6  25059  bposlem9  25062  lgsqrlem2  25117  lgsquadlem2  25151  chebbnd1lem2  25204  chebbnd1lem3  25205  chebbnd1  25206  chtppilimlem1  25207  chto1ub  25210  mulog2sumlem2  25269  chpdifbndlem1  25287  selberg3lem1  25291  pntrlog2bndlem2  25312  pntrlog2bndlem4  25314  pntpbnd1a  25319  pntpbnd1  25320  pntpbnd2  25321  pntibndlem1  25323  pntibndlem2  25325  pntibndlem3  25326  pntibnd  25327  pntlemb  25331  pntlemr  25336  pntlemf  25339  pnt  25348  ostth2lem1  25352  ostth2lem3  25369  ostth2lem4  25370  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  frgrogt3nreg  27384  friendshipgt3  27385  pjhthlem1  28378  psgnfzto1stlem  29978  1smat1  29998  sqsscirc1  30082  xrge0iifiso  30109  sgnsub  30734  signslema  30767  chtvalz  30835  hgt750lemd  30854  knoppndvlem12  32639  knoppndvlem14  32641  knoppndvlem15  32642  knoppndvlem17  32644  knoppndvlem20  32647  poimirlem6  33545  poimirlem7  33546  poimirlem8  33547  poimirlem15  33554  poimirlem20  33559  poimirlem28  33567  opnmbllem0  33575  itg2gt0cn  33595  ftc1cnnclem  33613  ftc1anc  33623  cntotbnd  33725  pellexlem5  37714  pellfundex  37767  pellfundrp  37769  rmspecfund  37791  monotuz  37823  jm3.1lem2  37902  jm3.1lem3  37903  imo72b2  38792  prmunb2  38827  neglt  39810  ltadd12dd  39872  infleinflem2  39900  sqrlearg  40098  lptre2pt  40190  0ellimcdiv  40199  limsup10exlem  40322  ioodvbdlimc1lem1  40464  iblspltprt  40507  itgspltprt  40513  stoweidlem7  40542  stoweidlem11  40546  stoweidlem13  40548  stoweidlem14  40549  stoweidlem26  40561  stoweidlem42  40577  stoweidlem52  40587  stoweidlem59  40594  stoweidlem60  40595  stoweidlem62  40597  wallispilem4  40603  wallispi  40605  stirlinglem1  40609  stirlinglem3  40611  stirlinglem6  40614  stirlinglem7  40615  stirlinglem10  40618  stirlinglem11  40619  dirkercncflem1  40638  dirkercncflem2  40639  fourierdlem10  40652  fourierdlem11  40653  fourierdlem12  40654  fourierdlem42  40684  fourierdlem47  40688  fourierdlem50  40691  fourierdlem51  40692  fourierdlem73  40714  fourierdlem79  40720  fourierdlem83  40724  fourierdlem103  40744  fourierdlem104  40745  sqwvfoura  40763  sqwvfourb  40764  fouriersw  40766  hoidmvlelem1  41130  hoiqssbllem2  41158  hspmbllem1  41161  pimrecltpos  41240  pimrecltneg  41254  smfaddlem1  41292  smflimlem3  41302  smflimlem4  41303  smfmullem1  41319
  Copyright terms: Public domain W3C validator