Theorem lelttrd 11363

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   class class class wbr 5109  ℝcr 11094   < clt 11238   ≤ cle 11239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-pre-lttri 11169  ax-pre-lttrn 11170

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  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 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244

This theorem is referenced by:  lt2msq1  12094  suprzcl  12671  ge0p1rp  13044  elfzolt3  13694  flflp1  13836  ltdifltdiv  13863  modsubdir  13972  seqf1olem1  14073  seqf1olem2  14074  expmulnbnd  14267  discr1  14271  faclbnd5  14330  bcp1nk  14349  hashfun  14470  swrds2  14973  abslt  15362  abs3lem  15386  fzomaxdiflem  15390  icodiamlt  15485  reccn2  15644  o1rlimmul  15666  caucvgrlem  15720  geomulcvg  15926  mertenslem1  15934  bpoly4  16108  ef01bndlem  16235  sin01bnd  16236  cos01bnd  16237  sinltx  16240  eirrlem  16255  rpnnen2lem11  16275  ruclem10  16290  bitsfzolem  16487  bitsfzo  16488  bitsinv1lem  16494  smueqlem  16543  pcfaclem  16953  pockthg  16961  prmreclem5  16975  1arith  16982  4sqlem11  17010  4sqlem12  17011  4sqlem13  17012  coe1tmmul2  22437  ssblex  24585  nlmvscnlem2  24842  nlmvscnlem1  24843  nrginvrcnlem  24848  blcvx  24955  icccmplem2  24981  reconnlem2  24985  metdcnlem  24994  icopnfcnv  25101  nmoleub2lem3  25274  ipcnlem2  25403  ipcnlem1  25404  minveclem3b  25587  minveclem3  25588  pjthlem1  25596  pmltpclem2  25608  ivthlem2  25611  ovollb2lem  25647  iundisj  25707  uniioombllem3  25744  opnmbllem  25760  itg2monolem3  25911  itg2cnlem2  25921  dveflem  26138  dvferm2lem  26145  lhop1lem  26172  dvcnvre  26178  ftc1a  26196  ftc1lem4  26198  coeeulem  26381  dgradd2  26425  aaliou2b  26504  ulmdvlem1  26563  itgulm  26571  radcnvlem1  26576  radcnvlt1  26581  radcnvle  26583  psercnlem1  26588  pserdvlem1  26590  pserdv  26592  abelthlem2  26595  abelthlem7  26601  cosordlem  26695  tanord1  26702  efif1olem1  26707  logcnlem3  26809  logcnlem4  26810  efopnlem1  26821  logtayl  26825  cxpcn3lem  26912  birthdaylem3  27118  efrlim  27134  lgamgulmlem2  27194  lgamucov  27202  ftalem1  27237  ftalem2  27238  ftalem5  27241  basellem1  27245  basellem3  27247  perfectlem2  27394  bposlem1  27448  bposlem3  27450  bposlem6  27453  lgsdirprm  27495  lgsqrlem2  27511  lgseisen  27543  lgsquadlem1  27544  lgsquadlem2  27545  2sqlem8  27590  2sqblem  27595  dchrvmasumiflem1  27665  pntrmax  27728  pntlemc  27759  pntlemg  27762  pntlemr  27766  axpaschlem  29290  axlowdimlem16  29307  clwwisshclwwslem  30365  smcnlem  31049  minvecolem3  31228  pjhthlem1  31743  nmcexi  32378  iundisjf  32934  iundisjfi  33141  psgnfzto1stlem  33420  esplyfval2  33955  esplyfval3  33962  cos9thpiminplylem1  34172  dya2icoseg  34667  reprgt  35008  hgt750lem  35038  tgoldbachgtde  35047  subfaclim  35680  bcprod  36230  dnicn  37101  unbdqndv2lem1  37118  unbdqndv2lem2  37119  knoppndvlem18  37138  poimirlem6  38297  poimirlem7  38298  poimirlem12  38303  poimirlem15  38306  poimirlem17  38308  poimirlem19  38310  poimirlem20  38311  poimirlem23  38314  poimirlem24  38315  opnmbllem0  38327  mblfinlem3  38330  mblfinlem4  38331  ftc1cnnclem  38362  ftc1anclem7  38370  isbnd3  38455  cntotbnd  38467  rrnequiv  38506  aks4d1p1p3  42856  aks4d1p1p2  42857  aks4d1p1p4  42858  aks4d1p1p7  42861  aks4d1p1p5  42862  aks4d1p5  42867  posbezout  42887  primrootlekpowne0  42892  aks6d1c5lem1  42923  2np3bcnp1  42931  sticksstones10  42942  sticksstones12a  42944  sticksstones22  42955  aks6d1c7lem1  42967  unitscyglem2  42983  flt4lem7  43411  fltnltalem  43414  fltnlta  43415  irrapxlem1  43569  pell14qrgapw  43623  monotoddzzfi  43689  ltrmynn0  43695  jm2.24nn  43706  acongeq  43730  jm2.26lem3  43748  jm3.1lem2  43765  binomcxplemnotnn0  45086  isosctrlem1ALT  45662  rfcnnnub  45776  zltlesub  46024  monoords  46036  supxrge  46074  infleinflem2  46106  uzubioo  46301  fmul01lt1lem1  46320  fmul01lt1lem2  46321  lptre2pt  46374  addlimc  46382  0ellimcdiv  46383  limclner  46385  climleltrp  46410  limsupubuzlem  46446  limsup10exlem  46506  icccncfext  46621  ioodvbdlimc1lem1  46665  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  dvnmul  46677  iblspltprt  46707  itgspltprt  46713  stoweidlem5  46739  stoweidlem11  46745  stoweidlem13  46747  stoweidlem14  46748  stoweidlem25  46759  stoweidlem26  46760  stoweidlem42  46776  stoweidlem59  46793  stoweid  46797  wallispilem3  46801  wallispilem4  46802  wallispilem5  46803  fourierdlem10  46851  fourierdlem11  46852  fourierdlem12  46853  fourierdlem15  46856  fourierdlem20  46861  fourierdlem24  46865  fourierdlem30  46871  fourierdlem31  46872  fourierdlem33  46874  fourierdlem40  46881  fourierdlem41  46882  fourierdlem42  46883  fourierdlem43  46884  fourierdlem44  46885  fourierdlem46  46886  fourierdlem47  46887  fourierdlem48  46888  fourierdlem50  46890  fourierdlem63  46903  fourierdlem64  46904  fourierdlem65  46905  fourierdlem73  46913  fourierdlem74  46914  fourierdlem75  46915  fourierdlem76  46916  fourierdlem77  46917  fourierdlem78  46918  fourierdlem79  46919  fourierdlem87  46927  fourierdlem91  46931  fourierdlem92  46932  fourierdlem103  46943  fourierdlem104  46944  fouriersw  46965  etransclem19  46987  etransclem23  46991  etransclem48  47016  ioorrnopnlem  47038  iundjiun  47194  omeiunltfirp  47253  caratheodorylem1  47260  hoicvr  47282  hoidmv1lelem2  47326  hoidmvlelem2  47330  hoiqssbllem2  47357  vonioolem1  47414  vonicclem1  47417  smflimlem4  47508  smfmullem1  47525  2tceilhalfelfzo1  48093  addmodne  48107  2timesltsqm1  48136  iccpartgt  48196  perfectALTVlem2  48507  bgoldbtbndlem2  48591  pgrple2abl  49165  logbpw2m1  49367  dignn0ldlem  49402  2itscp  49581