Theorem lelttrd 11342

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2143   class class class wbr 5101  ℝcr 11073   < clt 11217   ≤ cle 11218

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7719  ax-resscn 11131  ax-pre-lttri 11148  ax-pre-lttrn 11149

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6478  df-fun 6524  df-fn 6525  df-f 6526  df-f1 6527  df-fo 6528  df-f1o 6529  df-fv 6530  df-er 8679  df-en 8929  df-dom 8930  df-sdom 8931  df-pnf 11219  df-mnf 11220  df-xr 11221  df-ltxr 11222  df-le 11223

This theorem is referenced by:  lt2msq1  12077  suprzcl  12654  ge0p1rp  13027  elfzolt3  13676  flflp1  13818  ltdifltdiv  13845  modsubdir  13954  seqf1olem1  14055  seqf1olem2  14056  expmulnbnd  14249  discr1  14253  faclbnd5  14312  bcp1nk  14331  hashfun  14451  swrds2  14954  abslt  15343  abs3lem  15367  fzomaxdiflem  15371  icodiamlt  15466  reccn2  15625  o1rlimmul  15647  caucvgrlem  15701  geomulcvg  15907  mertenslem1  15915  bpoly4  16090  ef01bndlem  16217  sin01bnd  16218  cos01bnd  16219  sinltx  16222  eirrlem  16237  rpnnen2lem11  16257  ruclem10  16272  bitsfzolem  16469  bitsfzo  16470  bitsinv1lem  16476  smueqlem  16525  pcfaclem  16935  pockthg  16943  prmreclem5  16957  1arith  16964  4sqlem11  16992  4sqlem12  16993  4sqlem13  16994  coe1tmmul2  22340  ssblex  24489  nlmvscnlem2  24746  nlmvscnlem1  24747  nrginvrcnlem  24752  blcvx  24859  icccmplem2  24885  reconnlem2  24889  metdcnlem  24898  icopnfcnv  25005  nmoleub2lem3  25178  ipcnlem2  25307  ipcnlem1  25308  minveclem3b  25491  minveclem3  25492  pjthlem1  25500  pmltpclem2  25512  ivthlem2  25515  ovollb2lem  25551  iundisj  25611  uniioombllem3  25648  opnmbllem  25664  itg2monolem3  25815  itg2cnlem2  25825  dveflem  26042  dvferm2lem  26049  lhop1lem  26076  dvcnvre  26082  ftc1a  26100  ftc1lem4  26102  coeeulem  26285  dgradd2  26329  aaliou2b  26406  ulmdvlem1  26464  itgulm  26472  radcnvlem1  26477  radcnvlt1  26482  radcnvle  26484  psercnlem1  26489  pserdvlem1  26491  pserdv  26493  abelthlem2  26496  abelthlem7  26502  cosordlem  26596  tanord1  26603  efif1olem1  26608  logcnlem3  26710  logcnlem4  26711  efopnlem1  26722  logtayl  26726  cxpcn3lem  26813  birthdaylem3  27019  efrlim  27035  lgamgulmlem2  27095  lgamucov  27103  ftalem1  27138  ftalem2  27139  ftalem5  27142  basellem1  27146  basellem3  27148  perfectlem2  27295  bposlem1  27349  bposlem3  27351  bposlem6  27354  lgsdirprm  27396  lgsqrlem2  27412  lgseisen  27444  lgsquadlem1  27445  lgsquadlem2  27446  2sqlem8  27491  2sqblem  27496  dchrvmasumiflem1  27566  pntrmax  27629  pntlemc  27660  pntlemg  27663  pntlemr  27667  axpaschlem  29142  axlowdimlem16  29159  clwwisshclwwslem  30217  smcnlem  30901  minvecolem3  31080  pjhthlem1  31595  nmcexi  32230  iundisjf  32790  iundisjfi  32999  psgnfzto1stlem  33281  esplyfval2  33863  esplyfval3  33870  cos9thpiminplylem1  34080  dya2icoseg  34575  reprgt  34916  hgt750lem  34946  tgoldbachgtde  34955  subfaclim  35539  bcprod  36089  dnicn  36931  unbdqndv2lem1  36948  unbdqndv2lem2  36949  knoppndvlem18  36968  poimirlem6  38126  poimirlem7  38127  poimirlem12  38132  poimirlem15  38135  poimirlem17  38137  poimirlem19  38139  poimirlem20  38140  poimirlem23  38143  poimirlem24  38144  opnmbllem0  38156  mblfinlem3  38159  mblfinlem4  38160  ftc1cnnclem  38191  ftc1anclem7  38199  isbnd3  38284  cntotbnd  38296  rrnequiv  38335  aks4d1p1p3  42687  aks4d1p1p2  42688  aks4d1p1p4  42689  aks4d1p1p7  42692  aks4d1p1p5  42693  aks4d1p5  42698  posbezout  42718  primrootlekpowne0  42723  aks6d1c5lem1  42754  2np3bcnp1  42762  sticksstones10  42773  sticksstones12a  42775  sticksstones22  42786  aks6d1c7lem1  42798  unitscyglem2  42814  flt4lem7  43242  fltnltalem  43245  fltnlta  43246  irrapxlem1  43400  pell14qrgapw  43454  monotoddzzfi  43520  ltrmynn0  43526  jm2.24nn  43537  acongeq  43561  jm2.26lem3  43579  jm3.1lem2  43596  binomcxplemnotnn0  44933  isosctrlem1ALT  45510  rfcnnnub  45617  zltlesub  45865  monoords  45877  supxrge  45915  infleinflem2  45947  uzubioo  46142  fmul01lt1lem1  46161  fmul01lt1lem2  46162  lptre2pt  46215  addlimc  46223  0ellimcdiv  46224  limclner  46226  climleltrp  46251  limsupubuzlem  46287  limsup10exlem  46347  icccncfext  46462  ioodvbdlimc1lem1  46506  ioodvbdlimc1lem2  46507  ioodvbdlimc2lem  46509  dvnmul  46518  iblspltprt  46548  itgspltprt  46554  stoweidlem5  46580  stoweidlem11  46586  stoweidlem13  46588  stoweidlem14  46589  stoweidlem25  46600  stoweidlem26  46601  stoweidlem42  46617  stoweidlem59  46634  stoweid  46638  wallispilem3  46642  wallispilem4  46643  wallispilem5  46644  fourierdlem10  46692  fourierdlem11  46693  fourierdlem12  46694  fourierdlem15  46697  fourierdlem20  46702  fourierdlem24  46706  fourierdlem30  46712  fourierdlem31  46713  fourierdlem33  46715  fourierdlem40  46722  fourierdlem41  46723  fourierdlem42  46724  fourierdlem43  46725  fourierdlem44  46726  fourierdlem46  46727  fourierdlem47  46728  fourierdlem48  46729  fourierdlem50  46731  fourierdlem63  46744  fourierdlem64  46745  fourierdlem65  46746  fourierdlem73  46754  fourierdlem74  46755  fourierdlem75  46756  fourierdlem76  46757  fourierdlem77  46758  fourierdlem78  46759  fourierdlem79  46760  fourierdlem87  46768  fourierdlem91  46772  fourierdlem92  46773  fourierdlem103  46784  fourierdlem104  46785  fouriersw  46806  etransclem19  46828  etransclem23  46832  etransclem48  46857  ioorrnopnlem  46879  iundjiun  47035  omeiunltfirp  47094  caratheodorylem1  47101  hoicvr  47123  hoidmv1lelem2  47167  hoidmvlelem2  47171  hoiqssbllem2  47198  vonioolem1  47255  vonicclem1  47258  smflimlem4  47349  smfmullem1  47366  2tceilhalfelfzo1  47931  addmodne  47945  2timesltsqm1  47974  iccpartgt  48034  perfectALTVlem2  48345  bgoldbtbndlem2  48429  pgrple2abl  48988  logbpw2m1  49190  dignn0ldlem  49225  2itscp  49404