Theorem lelttrd 11468

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 11400	. . 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 2145   class class class wbr 5103  ℝcr 11199   < clt 11343   ≤ cle 11344

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751  ax-resscn 11257  ax-pre-lttri 11274  ax-pre-lttrn 11275

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-pnf 11345  df-mnf 11346  df-xr 11347  df-ltxr 11348  df-le 11349

This theorem is used by:  lt2msq1  12201  suprzcl  12779  ge0p1rp  13153  elfzolt3  13804  flflp1  13947  ltdifltdiv  13974  modsubdir  14083  seqf1olem1  14184  seqf1olem2  14185  expmulnbnd  14379  discr1  14383  faclbnd5  14442  bcp1nk  14461  hashfun  14582  swrds2  15091  abslt  15482  abs3lem  15506  fzomaxdiflem  15510  icodiamlt  15605  reccn2  15764  o1rlimmul  15786  caucvgrlem  15840  geomulcvg  16045  mertenslem1  16053  bpoly4  16225  ef01bndlem  16352  sin01bnd  16353  cos01bnd  16354  sinltx  16357  eirrlem  16372  rpnnen2lem11  16392  ruclem10  16407  bitsfzolem  16604  bitsfzo  16605  bitsinv1lem  16611  smueqlem  16660  pcfaclem  17076  pockthg  17084  prmreclem5  17098  1arith  17105  4sqlem11  17133  4sqlem12  17134  4sqlem13  17135  coe1tmmul2  22595  ssblex  24747  nlmvscnlem2  25004  nlmvscnlem1  25005  nrginvrcnlem  25010  blcvx  25117  icccmplem2  25143  reconnlem2  25147  metdcnlem  25156  icopnfcnv  25263  nmoleub2lem3  25436  ipcnlem2  25565  ipcnlem1  25566  minveclem3b  25749  minveclem3  25750  pjthlem1  25758  pmltpclem2  25770  ivthlem2  25773  ovollb2lem  25809  iundisj  25869  uniioombllem3  25906  opnmbllem  25922  itg2monolem3  26073  itg2cnlem2  26083  dveflem  26299  dvferm2lem  26306  lhop1lem  26333  dvcnvre  26339  ftc1a  26357  ftc1lem4  26359  coeeulem  26543  dgradd2  26587  aaliou2b  26668  ulmdvlem1  26727  itgulm  26735  radcnvlem1  26740  radcnvlt1  26745  radcnvle  26747  psercnlem1  26752  pserdvlem1  26754  pserdv  26756  abelthlem2  26759  abelthlem7  26765  cosordlem  26858  tanord1  26865  efif1olem1  26870  logcnlem3  26972  logcnlem4  26973  efopnlem1  26984  logtayl  26988  cxpcn3lem  27075  birthdaylem3  27281  efrlim  27297  lgamgulmlem2  27357  lgamucov  27365  ftalem1  27400  ftalem2  27401  ftalem5  27404  basellem1  27408  basellem3  27410  perfectlem2  27557  bposlem1  27611  bposlem3  27613  bposlem6  27616  lgsdirprm  27658  lgsqrlem2  27674  lgseisen  27706  lgsquadlem1  27707  lgsquadlem2  27708  2sqlem8  27753  2sqblem  27758  dchrvmasumiflem1  27828  pntrmax  27891  pntlemc  27922  pntlemg  27925  pntlemr  27929  flt4lem7  27989  axpaschlem  29518  axlowdimlem16  29535  clwwisshclwwslem  30605  smcnlem  31299  minvecolem3  31478  pjhthlem1  31993  nmcexi  32628  iundisjf  33183  iundisjfi  33388  psgnfzto1stlem  33661  esplyfval2  34197  esplyfval3  34204  cos9thpiminplylem1  34414  dya2icoseg  34909  reprgt  35250  hgt750lem  35280  tgoldbachgtde  35289  subfaclim  35953  bcprod  36503  dnicn  37358  unbdqndv2lem1  37375  unbdqndv2lem2  37376  knoppndvlem18  37395  poimirlem6  38544  poimirlem7  38545  poimirlem12  38550  poimirlem15  38553  poimirlem17  38555  poimirlem19  38557  poimirlem20  38558  poimirlem23  38561  poimirlem24  38562  opnmbllem0  38574  mblfinlem3  38577  mblfinlem4  38578  ftc1cnnclem  38609  ftc1anclem7  38617  isbnd3  38718  cntotbnd  38730  rrnequiv  38769  aks4d1p1p3  43119  aks4d1p1p2  43120  aks4d1p1p4  43121  aks4d1p1p7  43124  aks4d1p1p5  43125  aks4d1p5  43130  posbezout  43150  primrootlekpowne0  43155  aks6d1c5lem1  43186  2np3bcnp1  43194  sticksstones10  43205  sticksstones12a  43207  sticksstones22  43218  aks6d1c7lem1  43230  unitscyglem2  43246  fltnltalem  43673  fltnlta  43674  irrapxlem1  43828  pell14qrgapw  43882  monotoddzzfi  43948  ltrmynn0  43954  jm2.24nn  43965  acongeq  43989  jm2.26lem3  44007  jm3.1lem2  44024  binomcxplemnotnn0  45339  isosctrlem1ALT  45915  rfcnnnub  46052  zltlesub  46300  monoords  46312  supxrge  46349  infleinflem2  46381  uzubioo  46576  fmul01lt1lem1  46595  fmul01lt1lem2  46596  lptre2pt  46649  addlimc  46657  0ellimcdiv  46658  limclner  46660  climleltrp  46685  limsupubuzlem  46721  limsup10exlem  46781  icccncfext  46896  ioodvbdlimc1lem1  46940  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  dvnmul  46952  iblspltprt  46982  itgspltprt  46988  stoweidlem5  47014  stoweidlem11  47020  stoweidlem13  47022  stoweidlem14  47023  stoweidlem25  47034  stoweidlem26  47035  stoweidlem42  47051  stoweidlem59  47068  stoweid  47072  wallispilem3  47076  wallispilem4  47077  wallispilem5  47078  fourierdlem10  47126  fourierdlem11  47127  fourierdlem12  47128  fourierdlem15  47131  fourierdlem20  47136  fourierdlem24  47140  fourierdlem30  47146  fourierdlem31  47147  fourierdlem33  47149  fourierdlem40  47156  fourierdlem41  47157  fourierdlem42  47158  fourierdlem43  47159  fourierdlem44  47160  fourierdlem46  47161  fourierdlem47  47162  fourierdlem48  47163  fourierdlem50  47165  fourierdlem63  47178  fourierdlem64  47179  fourierdlem65  47180  fourierdlem73  47188  fourierdlem74  47189  fourierdlem75  47190  fourierdlem76  47191  fourierdlem77  47192  fourierdlem78  47193  fourierdlem79  47194  fourierdlem87  47202  fourierdlem91  47206  fourierdlem92  47207  fourierdlem103  47218  fourierdlem104  47219  fouriersw  47240  etransclem19  47262  etransclem23  47266  etransclem48  47291  ioorrnopnlem  47313  iundjiun  47469  omeiunltfirp  47528  caratheodorylem1  47535  hoicvr  47557  hoidmv1lelem2  47601  hoidmvlelem2  47605  hoiqssbllem2  47632  vonioolem1  47689  vonicclem1  47692  smflimlem4  47783  smfmullem1  47800  2tceilhalfelfzo1  48405  addmodne  48419  2timesltsqm1  48448  iccpartgt  48508  perfectALTVlem2  48819  bgoldbtbndlem2  48903  pgrple2abl  49476  logbpw2m1  49678  dignn0ldlem  49713  2itscp  49892