Theorem lelttrd 11332

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5107  ℝcr 11067   < clt 11208   ≤ cle 11209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-pre-lttri 11142  ax-pre-lttrn 11143

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214

This theorem is referenced by:  lt2msq1  12067  suprzcl  12614  ge0p1rp  12984  elfzolt3  13630  flflp1  13769  ltdifltdiv  13796  modsubdir  13905  seqf1olem1  14006  seqf1olem2  14007  expmulnbnd  14200  discr1  14204  faclbnd5  14263  bcp1nk  14282  hashfun  14402  swrds2  14906  abslt  15281  abs3lem  15305  fzomaxdiflem  15309  icodiamlt  15404  reccn2  15563  o1rlimmul  15585  caucvgrlem  15639  geomulcvg  15842  mertenslem1  15850  bpoly4  16025  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  sinltx  16157  eirrlem  16172  rpnnen2lem11  16192  ruclem10  16207  bitsfzolem  16404  bitsfzo  16405  bitsinv1lem  16411  smueqlem  16460  pcfaclem  16869  pockthg  16877  prmreclem5  16891  1arith  16898  4sqlem11  16926  4sqlem12  16927  4sqlem13  16928  coe1tmmul2  22162  ssblex  24316  nlmvscnlem2  24573  nlmvscnlem1  24574  nrginvrcnlem  24579  blcvx  24686  icccmplem2  24712  reconnlem2  24716  metdcnlem  24725  icopnfcnv  24840  nmoleub2lem3  25015  ipcnlem2  25144  ipcnlem1  25145  minveclem3b  25328  minveclem3  25329  pjthlem1  25337  pmltpclem2  25350  ivthlem2  25353  ovollb2lem  25389  iundisj  25449  uniioombllem3  25486  opnmbllem  25502  itg2monolem3  25653  itg2cnlem2  25663  dveflem  25883  dvferm2lem  25890  lhop1lem  25918  dvcnvre  25924  ftc1a  25944  ftc1lem4  25946  coeeulem  26129  dgradd2  26174  aaliou2b  26249  ulmdvlem1  26309  itgulm  26317  radcnvlem1  26322  radcnvlt1  26327  radcnvle  26329  psercnlem1  26335  pserdvlem1  26337  pserdv  26339  abelthlem2  26342  abelthlem7  26348  cosordlem  26439  tanord1  26446  efif1olem1  26451  logcnlem3  26553  logcnlem4  26554  efopnlem1  26565  logtayl  26569  cxpcn3lem  26657  birthdaylem3  26863  efrlim  26879  efrlimOLD  26880  lgamgulmlem2  26940  lgamucov  26948  ftalem1  26983  ftalem2  26984  ftalem5  26987  basellem1  26991  basellem3  26993  perfectlem2  27141  bposlem1  27195  bposlem3  27197  bposlem6  27200  lgsdirprm  27242  lgsqrlem2  27258  lgseisen  27290  lgsquadlem1  27291  lgsquadlem2  27292  2sqlem8  27337  2sqblem  27342  dchrvmasumiflem1  27412  pntrmax  27475  pntlemc  27506  pntlemg  27509  pntlemr  27513  axpaschlem  28867  axlowdimlem16  28884  clwwisshclwwslem  29943  smcnlem  30626  minvecolem3  30805  pjhthlem1  31320  nmcexi  31955  iundisjf  32518  iundisjfi  32719  psgnfzto1stlem  33057  cos9thpiminplylem1  33772  dya2icoseg  34268  reprgt  34612  hgt750lem  34642  tgoldbachgtde  34651  subfaclim  35175  bcprod  35725  dnicn  36480  unbdqndv2lem1  36497  unbdqndv2lem2  36498  knoppndvlem18  36517  poimirlem6  37620  poimirlem7  37621  poimirlem12  37626  poimirlem15  37629  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem23  37637  poimirlem24  37638  opnmbllem0  37650  mblfinlem3  37653  mblfinlem4  37654  ftc1cnnclem  37685  ftc1anclem7  37693  isbnd3  37778  cntotbnd  37790  rrnequiv  37829  aks4d1p1p3  42057  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p5  42068  posbezout  42088  primrootlekpowne0  42093  aks6d1c5lem1  42124  2np3bcnp1  42132  sticksstones10  42143  sticksstones12a  42145  sticksstones22  42156  aks6d1c7lem1  42168  unitscyglem2  42184  flt4lem7  42647  fltnltalem  42650  fltnlta  42651  irrapxlem1  42810  pell14qrgapw  42864  monotoddzzfi  42931  ltrmynn0  42937  jm2.24nn  42948  acongeq  42972  jm2.26lem3  42990  jm3.1lem2  43007  binomcxplemnotnn0  44345  isosctrlem1ALT  44923  rfcnnnub  45030  zltlesub  45283  monoords  45295  supxrge  45334  infleinflem2  45367  uzubioo  45563  fmul01lt1lem1  45582  fmul01lt1lem2  45583  lptre2pt  45638  addlimc  45646  0ellimcdiv  45647  limclner  45649  climleltrp  45674  limsupubuzlem  45710  limsup10exlem  45770  icccncfext  45885  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnmul  45941  iblspltprt  45971  itgspltprt  45977  stoweidlem5  46003  stoweidlem11  46009  stoweidlem13  46011  stoweidlem14  46012  stoweidlem25  46023  stoweidlem26  46024  stoweidlem42  46040  stoweidlem59  46057  stoweid  46061  wallispilem3  46065  wallispilem4  46066  wallispilem5  46067  fourierdlem10  46115  fourierdlem11  46116  fourierdlem12  46117  fourierdlem15  46120  fourierdlem20  46125  fourierdlem24  46129  fourierdlem30  46135  fourierdlem31  46136  fourierdlem33  46138  fourierdlem40  46145  fourierdlem41  46146  fourierdlem42  46147  fourierdlem43  46148  fourierdlem44  46149  fourierdlem46  46150  fourierdlem47  46151  fourierdlem48  46152  fourierdlem50  46154  fourierdlem63  46167  fourierdlem64  46168  fourierdlem65  46169  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem77  46181  fourierdlem78  46182  fourierdlem79  46183  fourierdlem87  46191  fourierdlem91  46195  fourierdlem92  46196  fourierdlem103  46207  fourierdlem104  46208  fouriersw  46229  etransclem19  46251  etransclem23  46255  etransclem48  46280  ioorrnopnlem  46302  iundjiun  46458  omeiunltfirp  46517  caratheodorylem1  46524  hoicvr  46546  hoidmv1lelem2  46590  hoidmvlelem2  46594  hoiqssbllem2  46621  vonioolem1  46678  vonicclem1  46681  smflimlem4  46772  smfmullem1  46789  2tceilhalfelfzo1  47333  addmodne  47345  iccpartgt  47428  perfectALTVlem2  47723  bgoldbtbndlem2  47807  pgrple2abl  48353  logbpw2m1  48556  dignn0ldlem  48591  2itscp  48770