Theorem lelttrd 11478

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 11410	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1398	. 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 712	1 ⊢ (𝜑 → 𝐴 < 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   class class class wbr 5105  ℝcr 11209   < clt 11353   ≤ cle 11354

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2196  ax-12 2215  ax-ext 2735  ax-sep 5251  ax-nul 5262  ax-pow 5330  ax-pr 5394  ax-un 7758  ax-resscn 11267  ax-pre-lttri 11284  ax-pre-lttrn 11285

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2101  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3416  df-v 3455  df-sbc 3742  df-csb 3851  df-ss 3900  df-dif 4049  df-in 4093  df-un 4153  df-nul 4281  df-if 4485  df-pw 4561  df-sn 4588  df-pr 4590  df-op 4838  df-uni 4870  df-br 5106  df-opab 5170  df-mpt 5189  df-id 5549  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6500  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-er 8728  df-en 8985  df-dom 8986  df-sdom 8987  df-pnf 11355  df-mnf 11356  df-xr 11357  df-ltxr 11358  df-le 11359

This theorem is used by:  lt2msq1  12211  suprzcl  12789  ge0p1rp  13163  elfzolt3  13814  flflp1  13957  ltdifltdiv  13984  modsubdir  14093  seqf1olem1  14194  seqf1olem2  14195  expmulnbnd  14389  discr1  14393  faclbnd5  14452  bcp1nk  14471  hashfun  14592  swrds2  15103  abslt  15494  abs3lem  15518  fzomaxdiflem  15522  icodiamlt  15617  reccn2  15776  o1rlimmul  15798  caucvgrlem  15852  geomulcvg  16057  mertenslem1  16065  bpoly4  16237  ef01bndlem  16364  sin01bnd  16365  cos01bnd  16366  sinltx  16369  eirrlem  16384  rpnnen2lem11  16404  ruclem10  16419  bitsfzolem  16616  bitsfzo  16617  bitsinv1lem  16623  smueqlem  16672  pcfaclem  17088  pockthg  17096  prmreclem5  17110  1arith  17117  4sqlem11  17145  4sqlem12  17146  4sqlem13  17147  coe1tmmul2  22607  ssblex  24759  nlmvscnlem2  25016  nlmvscnlem1  25017  nrginvrcnlem  25022  blcvx  25129  icccmplem2  25155  reconnlem2  25159  metdcnlem  25168  icopnfcnv  25275  nmoleub2lem3  25448  ipcnlem2  25577  ipcnlem1  25578  minveclem3b  25761  minveclem3  25762  pjthlem1  25770  pmltpclem2  25782  ivthlem2  25785  ovollb2lem  25821  iundisj  25881  uniioombllem3  25918  opnmbllem  25934  itg2monolem3  26085  itg2cnlem2  26095  dveflem  26311  dvferm2lem  26318  lhop1lem  26345  dvcnvre  26351  ftc1a  26369  ftc1lem4  26371  coeeulem  26555  dgradd2  26599  aaliou2b  26680  ulmdvlem1  26739  itgulm  26747  radcnvlem1  26752  radcnvlt1  26757  radcnvle  26759  psercnlem1  26764  pserdvlem1  26766  pserdv  26768  abelthlem2  26771  abelthlem7  26777  cosordlem  26870  tanord1  26877  efif1olem1  26882  logcnlem3  26984  logcnlem4  26985  efopnlem1  26996  logtayl  27000  cxpcn3lem  27087  birthdaylem3  27293  efrlim  27309  lgamgulmlem2  27369  lgamucov  27377  ftalem1  27412  ftalem2  27413  ftalem5  27416  basellem1  27420  basellem3  27422  perfectlem2  27569  bposlem1  27623  bposlem3  27625  bposlem6  27628  lgsdirprm  27670  lgsqrlem2  27686  lgseisen  27718  lgsquadlem1  27719  lgsquadlem2  27720  2sqlem8  27765  2sqblem  27770  dchrvmasumiflem1  27840  pntrmax  27903  pntlemc  27934  pntlemg  27937  pntlemr  27941  flt4lem7  28001  axpaschlem  29530  axlowdimlem16  29547  clwwisshclwwslem  30617  smcnlem  31311  minvecolem3  31490  pjhthlem1  32005  nmcexi  32640  iundisjf  33237  iundisjfi  33441  psgnfzto1stlem  33714  esplyfval2  34250  esplyfval3  34257  cos9thpiminplylem1  34467  dya2icoseg  34962  reprgt  35303  hgt750lem  35333  tgoldbachgtde  35342  subfaclim  36074  bcprod  36630  dnicn  37485  unbdqndv2lem1  37502  unbdqndv2lem2  37503  knoppndvlem18  37522  poimirlem6  38684  poimirlem7  38685  poimirlem12  38690  poimirlem15  38693  poimirlem17  38695  poimirlem19  38697  poimirlem20  38698  poimirlem23  38701  poimirlem24  38702  opnmbllem0  38714  mblfinlem3  38717  mblfinlem4  38718  ftc1cnnclem  38749  ftc1anclem7  38757  isbnd3  38858  cntotbnd  38870  rrnequiv  38909  aks4d1p1p3  43259  aks4d1p1p2  43260  aks4d1p1p4  43261  aks4d1p1p7  43264  aks4d1p1p5  43265  aks4d1p5  43270  posbezout  43290  primrootlekpowne0  43295  aks6d1c5lem1  43326  2np3bcnp1  43334  sticksstones10  43345  sticksstones12a  43347  sticksstones22  43358  aks6d1c7lem1  43370  unitscyglem2  43386  fltnltalem  43813  fltnlta  43814  irrapxlem1  43969  pell14qrgapw  44023  monotoddzzfi  44089  ltrmynn0  44095  jm2.24nn  44106  acongeq  44130  jm2.26lem3  44148  jm3.1lem2  44165  binomcxplemnotnn0  45480  isosctrlem1ALT  46055  rfcnnnub  46192  zltlesub  46440  monoords  46452  supxrge  46489  infleinflem2  46521  uzubioo  46716  fmul01lt1lem1  46735  fmul01lt1lem2  46736  lptre2pt  46789  addlimc  46797  0ellimcdiv  46798  limclner  46800  climleltrp  46825  limsupubuzlem  46861  limsup10exlem  46921  icccncfext  47036  ioodvbdlimc1lem1  47080  ioodvbdlimc1lem2  47081  ioodvbdlimc2lem  47083  dvnmul  47092  iblspltprt  47122  itgspltprt  47128  stoweidlem5  47154  stoweidlem11  47160  stoweidlem13  47162  stoweidlem14  47163  stoweidlem25  47174  stoweidlem26  47175  stoweidlem42  47191  stoweidlem59  47208  stoweid  47212  wallispilem3  47216  wallispilem4  47217  wallispilem5  47218  fourierdlem10  47266  fourierdlem11  47267  fourierdlem12  47268  fourierdlem15  47271  fourierdlem20  47276  fourierdlem24  47280  fourierdlem30  47286  fourierdlem31  47287  fourierdlem33  47289  fourierdlem40  47296  fourierdlem41  47297  fourierdlem42  47298  fourierdlem43  47299  fourierdlem44  47300  fourierdlem46  47301  fourierdlem47  47302  fourierdlem48  47303  fourierdlem50  47305  fourierdlem63  47318  fourierdlem64  47319  fourierdlem65  47320  fourierdlem73  47328  fourierdlem74  47329  fourierdlem75  47330  fourierdlem76  47331  fourierdlem77  47332  fourierdlem78  47333  fourierdlem79  47334  fourierdlem87  47342  fourierdlem91  47346  fourierdlem92  47347  fourierdlem103  47358  fourierdlem104  47359  fouriersw  47380  etransclem19  47402  etransclem23  47406  etransclem48  47431  ioorrnopnlem  47453  iundjiun  47609  omeiunltfirp  47668  caratheodorylem1  47675  hoicvr  47697  hoidmv1lelem2  47741  hoidmvlelem2  47745  hoiqssbllem2  47772  vonioolem1  47829  vonicclem1  47832  smflimlem4  47923  smfmullem1  47940  2tceilhalfelfzo1  48545  addmodne  48559  2timesltsqm1  48588  iccpartgt  48648  perfectALTVlem2  48959  bgoldbtbndlem2  49043  pgrple2abl  49616  logbpw2m1  49818  dignn0ldlem  49853  2itscp  50032