Theorem lelttrd 11289

Description: Transitive law deduction for 'less than or equal to', 'less than'. (Contributed by NM, 8-Jan-2006.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
letrd.3	⊢ (𝜑 → 𝐶 ∈ ℝ)
lelttrd.4	⊢ (𝜑 → 𝐴 ≤ 𝐵)
lelttrd.5	⊢ (𝜑 → 𝐵 < 𝐶)

Assertion

Ref	Expression
lelttrd	⊢ (𝜑 → 𝐴 < 𝐶)

Proof of Theorem lelttrd

Step	Hyp	Ref	Expression
1		lelttrd.4	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
2		lelttrd.5	. 2 ⊢ (𝜑 → 𝐵 < 𝐶)
3		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		letrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		lelttr 11221	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1373	. 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 699	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   class class class wbr 5096  ℝcr 11023   < clt 11164   ≤ cle 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-pre-lttri 11098  ax-pre-lttrn 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170

This theorem is referenced by:  lt2msq1  12024  suprzcl  12570  ge0p1rp  12936  elfzolt3  13583  flflp1  13725  ltdifltdiv  13752  modsubdir  13861  seqf1olem1  13962  seqf1olem2  13963  expmulnbnd  14156  discr1  14160  faclbnd5  14219  bcp1nk  14238  hashfun  14358  swrds2  14861  abslt  15236  abs3lem  15260  fzomaxdiflem  15264  icodiamlt  15359  reccn2  15518  o1rlimmul  15540  caucvgrlem  15594  geomulcvg  15797  mertenslem1  15805  bpoly4  15980  ef01bndlem  16107  sin01bnd  16108  cos01bnd  16109  sinltx  16112  eirrlem  16127  rpnnen2lem11  16147  ruclem10  16162  bitsfzolem  16359  bitsfzo  16360  bitsinv1lem  16366  smueqlem  16415  pcfaclem  16824  pockthg  16832  prmreclem5  16846  1arith  16853  4sqlem11  16881  4sqlem12  16882  4sqlem13  16883  coe1tmmul2  22216  ssblex  24370  nlmvscnlem2  24627  nlmvscnlem1  24628  nrginvrcnlem  24633  blcvx  24740  icccmplem2  24766  reconnlem2  24770  metdcnlem  24779  icopnfcnv  24894  nmoleub2lem3  25069  ipcnlem2  25198  ipcnlem1  25199  minveclem3b  25382  minveclem3  25383  pjthlem1  25391  pmltpclem2  25404  ivthlem2  25407  ovollb2lem  25443  iundisj  25503  uniioombllem3  25540  opnmbllem  25556  itg2monolem3  25707  itg2cnlem2  25717  dveflem  25937  dvferm2lem  25944  lhop1lem  25972  dvcnvre  25978  ftc1a  25998  ftc1lem4  26000  coeeulem  26183  dgradd2  26228  aaliou2b  26303  ulmdvlem1  26363  itgulm  26371  radcnvlem1  26376  radcnvlt1  26381  radcnvle  26383  psercnlem1  26389  pserdvlem1  26391  pserdv  26393  abelthlem2  26396  abelthlem7  26402  cosordlem  26493  tanord1  26500  efif1olem1  26505  logcnlem3  26607  logcnlem4  26608  efopnlem1  26619  logtayl  26623  cxpcn3lem  26711  birthdaylem3  26917  efrlim  26933  efrlimOLD  26934  lgamgulmlem2  26994  lgamucov  27002  ftalem1  27037  ftalem2  27038  ftalem5  27041  basellem1  27045  basellem3  27047  perfectlem2  27195  bposlem1  27249  bposlem3  27251  bposlem6  27254  lgsdirprm  27296  lgsqrlem2  27312  lgseisen  27344  lgsquadlem1  27345  lgsquadlem2  27346  2sqlem8  27391  2sqblem  27396  dchrvmasumiflem1  27466  pntrmax  27529  pntlemc  27560  pntlemg  27563  pntlemr  27567  axpaschlem  28962  axlowdimlem16  28979  clwwisshclwwslem  30038  smcnlem  30721  minvecolem3  30900  pjhthlem1  31415  nmcexi  32050  iundisjf  32613  iundisjfi  32825  psgnfzto1stlem  33131  esplyfval2  33672  esplyfval3  33679  cos9thpiminplylem1  33888  dya2icoseg  34383  reprgt  34727  hgt750lem  34757  tgoldbachgtde  34766  subfaclim  35331  bcprod  35881  dnicn  36635  unbdqndv2lem1  36652  unbdqndv2lem2  36653  knoppndvlem18  36672  poimirlem6  37766  poimirlem7  37767  poimirlem12  37772  poimirlem15  37775  poimirlem17  37777  poimirlem19  37779  poimirlem20  37780  poimirlem23  37783  poimirlem24  37784  opnmbllem0  37796  mblfinlem3  37799  mblfinlem4  37800  ftc1cnnclem  37831  ftc1anclem7  37839  isbnd3  37924  cntotbnd  37936  rrnequiv  37975  aks4d1p1p3  42262  aks4d1p1p2  42263  aks4d1p1p4  42264  aks4d1p1p7  42267  aks4d1p1p5  42268  aks4d1p5  42273  posbezout  42293  primrootlekpowne0  42298  aks6d1c5lem1  42329  2np3bcnp1  42337  sticksstones10  42348  sticksstones12a  42350  sticksstones22  42361  aks6d1c7lem1  42373  unitscyglem2  42389  flt4lem7  42844  fltnltalem  42847  fltnlta  42848  irrapxlem1  43006  pell14qrgapw  43060  monotoddzzfi  43126  ltrmynn0  43132  jm2.24nn  43143  acongeq  43167  jm2.26lem3  43185  jm3.1lem2  43202  binomcxplemnotnn0  44539  isosctrlem1ALT  45116  rfcnnnub  45223  zltlesub  45475  monoords  45487  supxrge  45525  infleinflem2  45557  uzubioo  45753  fmul01lt1lem1  45772  fmul01lt1lem2  45773  lptre2pt  45826  addlimc  45834  0ellimcdiv  45835  limclner  45837  climleltrp  45862  limsupubuzlem  45898  limsup10exlem  45958  icccncfext  46073  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnmul  46129  iblspltprt  46159  itgspltprt  46165  stoweidlem5  46191  stoweidlem11  46197  stoweidlem13  46199  stoweidlem14  46200  stoweidlem25  46211  stoweidlem26  46212  stoweidlem42  46228  stoweidlem59  46245  stoweid  46249  wallispilem3  46253  wallispilem4  46254  wallispilem5  46255  fourierdlem10  46303  fourierdlem11  46304  fourierdlem12  46305  fourierdlem15  46308  fourierdlem20  46313  fourierdlem24  46317  fourierdlem30  46323  fourierdlem31  46324  fourierdlem33  46326  fourierdlem40  46333  fourierdlem41  46334  fourierdlem42  46335  fourierdlem43  46336  fourierdlem44  46337  fourierdlem46  46338  fourierdlem47  46339  fourierdlem48  46340  fourierdlem50  46342  fourierdlem63  46355  fourierdlem64  46356  fourierdlem65  46357  fourierdlem73  46365  fourierdlem74  46366  fourierdlem75  46367  fourierdlem76  46368  fourierdlem77  46369  fourierdlem78  46370  fourierdlem79  46371  fourierdlem87  46379  fourierdlem91  46383  fourierdlem92  46384  fourierdlem103  46395  fourierdlem104  46396  fouriersw  46417  etransclem19  46439  etransclem23  46443  etransclem48  46468  ioorrnopnlem  46490  iundjiun  46646  omeiunltfirp  46705  caratheodorylem1  46712  hoicvr  46734  hoidmv1lelem2  46778  hoidmvlelem2  46782  hoiqssbllem2  46809  vonioolem1  46866  vonicclem1  46869  smflimlem4  46960  smfmullem1  46977  2tceilhalfelfzo1  47520  addmodne  47532  iccpartgt  47615  perfectALTVlem2  47910  bgoldbtbndlem2  47994  pgrple2abl  48553  logbpw2m1  48755  dignn0ldlem  48790  2itscp  48969