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

Theorem lttrd 10790
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 10706 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
73, 4, 5, 6syl3anc 1363 . 2 (𝜑 → ((𝐴 < 𝐵𝐵 < 𝐶) → 𝐴 < 𝐶))
81, 2, 7mp2and 695 1 (𝜑𝐴 < 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105   class class class wbr 5058  cr 10525   < clt 10664
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-resscn 10583  ax-pre-lttrn 10601
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-er 8279  df-en 8499  df-dom 8500  df-sdom 8501  df-pnf 10666  df-mnf 10667  df-ltxr 10669
This theorem is referenced by:  nnne0  11660  expgt1  13457  ltexp2a  13520  expcan  13523  ltexp2  13524  leexp2  13525  expnlbnd2  13585  expmulnbnd  13586  reccn2  14943  efgt1  15459  tanhlt1  15503  ruclem2  15575  isprm7  16042  pythagtriplem13  16154  fldivp1  16223  4sqlem12  16282  sylow1lem1  18654  telgsums  19044  chfacffsupp  21394  chfacfscmul0  21396  chfacfpmmul0  21400  nrginvrcnlem  23229  iccntr  23358  icccmplem2  23360  opnreen  23368  pjthlem1  23969  pmltpclem2  23979  ovollb2lem  24018  opnmbllem  24131  volivth  24137  lhop1lem  24539  dvcnvrelem1  24543  dvcvx  24546  ftc1lem4  24565  aaliou3lem7  24867  ulmdvlem1  24917  reeff1olem  24963  pilem2  24969  pilem3  24970  tangtx  25020  tanord1  25048  tanord  25049  rplogcl  25114  logimul  25124  logcnlem3  25154  efopnlem1  25166  cxplt  25204  cxple  25205  cxpcn3lem  25255  asinsin  25397  atanlogaddlem  25418  atanlogsublem  25420  cxp2limlem  25481  cxp2lim  25482  zetacvg  25520  lgamucov  25543  lgamcvg2  25560  ftalem1  25578  mersenne  25731  bposlem2  25789  bposlem6  25793  bposlem9  25796  lgsqrlem2  25851  lgsquadlem2  25885  chebbnd1lem2  25974  chebbnd1lem3  25975  chebbnd1  25976  chtppilimlem1  25977  chto1ub  25980  mulog2sumlem2  26039  chpdifbndlem1  26057  selberg3lem1  26061  pntrlog2bndlem2  26082  pntrlog2bndlem4  26084  pntpbnd1a  26089  pntpbnd1  26090  pntpbnd2  26091  pntibndlem1  26093  pntibndlem2  26095  pntibndlem3  26096  pntibnd  26097  pntlemb  26101  pntlemr  26106  pntlemf  26109  pnt  26118  ostth2lem1  26122  ostth2lem3  26139  ostth2lem4  26140  wwlksext2clwwlk  27764  frgrogt3nreg  28104  friendshipgt3  28105  pjhthlem1  29096  psgnfzto1stlem  30670  1smat1  30969  sqsscirc1  31051  xrge0iifiso  31078  sgnsub  31702  signslema  31732  chtvalz  31800  hgt750lemd  31819  knoppndvlem12  33760  knoppndvlem14  33762  knoppndvlem15  33763  knoppndvlem17  33765  knoppndvlem20  33768  poimirlem6  34780  poimirlem7  34781  poimirlem8  34782  poimirlem15  34789  poimirlem20  34794  poimirlem28  34802  opnmbllem0  34810  itg2gt0cn  34829  ftc1cnnclem  34847  ftc1anc  34857  cntotbnd  34957  fltnlta  39155  pellexlem5  39310  pellfundex  39363  pellfundrp  39365  rmspecfund  39386  monotuz  39418  jm3.1lem2  39495  jm3.1lem3  39496  imo72b2  40406  prmunb2  40523  neglt  41430  ltadd12dd  41491  infleinflem2  41519  sqrlearg  41709  lptre2pt  41801  0ellimcdiv  41810  limsup10exlem  41933  ioodvbdlimc1lem1  42096  iblspltprt  42138  itgspltprt  42144  stoweidlem7  42173  stoweidlem11  42177  stoweidlem13  42179  stoweidlem14  42180  stoweidlem26  42192  stoweidlem42  42208  stoweidlem52  42218  stoweidlem59  42225  stoweidlem60  42226  stoweidlem62  42228  wallispilem4  42234  wallispi  42236  stirlinglem1  42240  stirlinglem3  42242  stirlinglem6  42245  stirlinglem7  42246  stirlinglem10  42249  stirlinglem11  42250  dirkercncflem1  42269  dirkercncflem2  42270  fourierdlem10  42283  fourierdlem11  42284  fourierdlem12  42285  fourierdlem42  42315  fourierdlem47  42319  fourierdlem50  42322  fourierdlem51  42323  fourierdlem73  42345  fourierdlem79  42351  fourierdlem83  42355  fourierdlem103  42375  fourierdlem104  42376  sqwvfoura  42394  sqwvfourb  42395  fouriersw  42397  hoidmvlelem1  42758  hoiqssbllem2  42786  hspmbllem1  42789  pimrecltpos  42868  pimrecltneg  42882  smfaddlem1  42920  smflimlem3  42930  smflimlem4  42931  smfmullem1  42947  fpprel2  43753  eenglngeehlnmlem2  44623
  Copyright terms: Public domain W3C validator