Theorem lelttrd 11304

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5085  ℝcr 11037   < clt 11179   ≤ cle 11180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-er 8643  df-en 8894  df-dom 8895  df-sdom 8896  df-pnf 11181  df-mnf 11182  df-xr 11183  df-ltxr 11184  df-le 11185

This theorem is referenced by:  lt2msq1  12040  suprzcl  12609  ge0p1rp  12975  elfzolt3  13624  flflp1  13766  ltdifltdiv  13793  modsubdir  13902  seqf1olem1  14003  seqf1olem2  14004  expmulnbnd  14197  discr1  14201  faclbnd5  14260  bcp1nk  14279  hashfun  14399  swrds2  14902  abslt  15277  abs3lem  15301  fzomaxdiflem  15305  icodiamlt  15400  reccn2  15559  o1rlimmul  15581  caucvgrlem  15635  geomulcvg  15841  mertenslem1  15849  bpoly4  16024  ef01bndlem  16151  sin01bnd  16152  cos01bnd  16153  sinltx  16156  eirrlem  16171  rpnnen2lem11  16191  ruclem10  16206  bitsfzolem  16403  bitsfzo  16404  bitsinv1lem  16410  smueqlem  16459  pcfaclem  16869  pockthg  16877  prmreclem5  16891  1arith  16898  4sqlem11  16926  4sqlem12  16927  4sqlem13  16928  coe1tmmul2  22241  ssblex  24393  nlmvscnlem2  24650  nlmvscnlem1  24651  nrginvrcnlem  24656  blcvx  24763  icccmplem2  24789  reconnlem2  24793  metdcnlem  24802  icopnfcnv  24909  nmoleub2lem3  25082  ipcnlem2  25211  ipcnlem1  25212  minveclem3b  25395  minveclem3  25396  pjthlem1  25404  pmltpclem2  25416  ivthlem2  25419  ovollb2lem  25455  iundisj  25515  uniioombllem3  25552  opnmbllem  25568  itg2monolem3  25719  itg2cnlem2  25729  dveflem  25946  dvferm2lem  25953  lhop1lem  25980  dvcnvre  25986  ftc1a  26004  ftc1lem4  26006  coeeulem  26189  dgradd2  26233  aaliou2b  26307  ulmdvlem1  26365  itgulm  26373  radcnvlem1  26378  radcnvlt1  26383  radcnvle  26385  psercnlem1  26390  pserdvlem1  26392  pserdv  26394  abelthlem2  26397  abelthlem7  26403  cosordlem  26494  tanord1  26501  efif1olem1  26506  logcnlem3  26608  logcnlem4  26609  efopnlem1  26620  logtayl  26624  cxpcn3lem  26711  birthdaylem3  26917  efrlim  26933  lgamgulmlem2  26993  lgamucov  27001  ftalem1  27036  ftalem2  27037  ftalem5  27040  basellem1  27044  basellem3  27046  perfectlem2  27193  bposlem1  27247  bposlem3  27249  bposlem6  27252  lgsdirprm  27294  lgsqrlem2  27310  lgseisen  27342  lgsquadlem1  27343  lgsquadlem2  27344  2sqlem8  27389  2sqblem  27394  dchrvmasumiflem1  27464  pntrmax  27527  pntlemc  27558  pntlemg  27561  pntlemr  27565  axpaschlem  29009  axlowdimlem16  29026  clwwisshclwwslem  30084  smcnlem  30768  minvecolem3  30947  pjhthlem1  31462  nmcexi  32097  iundisjf  32659  iundisjfi  32869  psgnfzto1stlem  33161  esplyfval2  33709  esplyfval3  33716  cos9thpiminplylem1  33926  dya2icoseg  34421  reprgt  34765  hgt750lem  34795  tgoldbachgtde  34804  subfaclim  35370  bcprod  35920  dnicn  36752  unbdqndv2lem1  36769  unbdqndv2lem2  36770  knoppndvlem18  36789  poimirlem6  37947  poimirlem7  37948  poimirlem12  37953  poimirlem15  37956  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem23  37964  poimirlem24  37965  opnmbllem0  37977  mblfinlem3  37980  mblfinlem4  37981  ftc1cnnclem  38012  ftc1anclem7  38020  isbnd3  38105  cntotbnd  38117  rrnequiv  38156  aks4d1p1p3  42508  aks4d1p1p2  42509  aks4d1p1p4  42510  aks4d1p1p7  42513  aks4d1p1p5  42514  aks4d1p5  42519  posbezout  42539  primrootlekpowne0  42544  aks6d1c5lem1  42575  2np3bcnp1  42583  sticksstones10  42594  sticksstones12a  42596  sticksstones22  42607  aks6d1c7lem1  42619  unitscyglem2  42635  flt4lem7  43092  fltnltalem  43095  fltnlta  43096  irrapxlem1  43250  pell14qrgapw  43304  monotoddzzfi  43370  ltrmynn0  43376  jm2.24nn  43387  acongeq  43411  jm2.26lem3  43429  jm3.1lem2  43446  binomcxplemnotnn0  44783  isosctrlem1ALT  45360  rfcnnnub  45467  zltlesub  45718  monoords  45730  supxrge  45768  infleinflem2  45800  uzubioo  45995  fmul01lt1lem1  46014  fmul01lt1lem2  46015  lptre2pt  46068  addlimc  46076  0ellimcdiv  46077  limclner  46079  climleltrp  46104  limsupubuzlem  46140  limsup10exlem  46200  icccncfext  46315  ioodvbdlimc1lem1  46359  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnmul  46371  iblspltprt  46401  itgspltprt  46407  stoweidlem5  46433  stoweidlem11  46439  stoweidlem13  46441  stoweidlem14  46442  stoweidlem25  46453  stoweidlem26  46454  stoweidlem42  46470  stoweidlem59  46487  stoweid  46491  wallispilem3  46495  wallispilem4  46496  wallispilem5  46497  fourierdlem10  46545  fourierdlem11  46546  fourierdlem12  46547  fourierdlem15  46550  fourierdlem20  46555  fourierdlem24  46559  fourierdlem30  46565  fourierdlem31  46566  fourierdlem33  46568  fourierdlem40  46575  fourierdlem41  46576  fourierdlem42  46577  fourierdlem43  46578  fourierdlem44  46579  fourierdlem46  46580  fourierdlem47  46581  fourierdlem48  46582  fourierdlem50  46584  fourierdlem63  46597  fourierdlem64  46598  fourierdlem65  46599  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem77  46611  fourierdlem78  46612  fourierdlem79  46613  fourierdlem87  46621  fourierdlem91  46625  fourierdlem92  46626  fourierdlem103  46637  fourierdlem104  46638  fouriersw  46659  etransclem19  46681  etransclem23  46685  etransclem48  46710  ioorrnopnlem  46732  iundjiun  46888  omeiunltfirp  46947  caratheodorylem1  46954  hoicvr  46976  hoidmv1lelem2  47020  hoidmvlelem2  47024  hoiqssbllem2  47051  vonioolem1  47108  vonicclem1  47111  smflimlem4  47202  smfmullem1  47219  2tceilhalfelfzo1  47784  addmodne  47798  2timesltsqm1  47827  iccpartgt  47887  perfectALTVlem2  48198  bgoldbtbndlem2  48282  pgrple2abl  48841  logbpw2m1  49043  dignn0ldlem  49078  2itscp  49257