Theorem lelttrd 11391

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5119  ℝcr 11126   < clt 11267   ≤ cle 11268

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-resscn 11184  ax-pre-lttri 11201  ax-pre-lttrn 11202

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273

This theorem is referenced by:  lt2msq1  12124  suprzcl  12671  ge0p1rp  13038  elfzolt3  13684  flflp1  13822  ltdifltdiv  13849  modsubdir  13956  seqf1olem1  14057  seqf1olem2  14058  expmulnbnd  14251  discr1  14255  faclbnd5  14314  bcp1nk  14333  hashfun  14453  swrds2  14957  abslt  15331  abs3lem  15355  fzomaxdiflem  15359  icodiamlt  15452  reccn2  15611  o1rlimmul  15633  caucvgrlem  15687  geomulcvg  15890  mertenslem1  15898  bpoly4  16073  ef01bndlem  16200  sin01bnd  16201  cos01bnd  16202  sinltx  16205  eirrlem  16220  rpnnen2lem11  16240  ruclem10  16255  bitsfzolem  16451  bitsfzo  16452  bitsinv1lem  16458  smueqlem  16507  pcfaclem  16916  pockthg  16924  prmreclem5  16938  1arith  16945  4sqlem11  16973  4sqlem12  16974  4sqlem13  16975  coe1tmmul2  22211  ssblex  24365  nlmvscnlem2  24622  nlmvscnlem1  24623  nrginvrcnlem  24628  blcvx  24735  icccmplem2  24761  reconnlem2  24765  metdcnlem  24774  icopnfcnv  24889  nmoleub2lem3  25064  ipcnlem2  25194  ipcnlem1  25195  minveclem3b  25378  minveclem3  25379  pjthlem1  25387  pmltpclem2  25400  ivthlem2  25403  ovollb2lem  25439  iundisj  25499  uniioombllem3  25536  opnmbllem  25552  itg2monolem3  25703  itg2cnlem2  25713  dveflem  25933  dvferm2lem  25940  lhop1lem  25968  dvcnvre  25974  ftc1a  25994  ftc1lem4  25996  coeeulem  26179  dgradd2  26224  aaliou2b  26299  ulmdvlem1  26359  itgulm  26367  radcnvlem1  26372  radcnvlt1  26377  radcnvle  26379  psercnlem1  26385  pserdvlem1  26387  pserdv  26389  abelthlem2  26392  abelthlem7  26398  cosordlem  26489  tanord1  26496  efif1olem1  26501  logcnlem3  26603  logcnlem4  26604  efopnlem1  26615  logtayl  26619  cxpcn3lem  26707  birthdaylem3  26913  efrlim  26929  efrlimOLD  26930  lgamgulmlem2  26990  lgamucov  26998  ftalem1  27033  ftalem2  27034  ftalem5  27037  basellem1  27041  basellem3  27043  perfectlem2  27191  bposlem1  27245  bposlem3  27247  bposlem6  27250  lgsdirprm  27292  lgsqrlem2  27308  lgseisen  27340  lgsquadlem1  27341  lgsquadlem2  27342  2sqlem8  27387  2sqblem  27392  dchrvmasumiflem1  27462  pntrmax  27525  pntlemc  27556  pntlemg  27559  pntlemr  27563  axpaschlem  28865  axlowdimlem16  28882  clwwisshclwwslem  29941  smcnlem  30624  minvecolem3  30803  pjhthlem1  31318  nmcexi  31953  iundisjf  32516  iundisjfi  32719  psgnfzto1stlem  33057  cos9thpiminplylem1  33762  dya2icoseg  34255  reprgt  34599  hgt750lem  34629  tgoldbachgtde  34638  subfaclim  35156  bcprod  35701  dnicn  36456  unbdqndv2lem1  36473  unbdqndv2lem2  36474  knoppndvlem18  36493  poimirlem6  37596  poimirlem7  37597  poimirlem12  37602  poimirlem15  37605  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem23  37613  poimirlem24  37614  opnmbllem0  37626  mblfinlem3  37629  mblfinlem4  37630  ftc1cnnclem  37661  ftc1anclem7  37669  isbnd3  37754  cntotbnd  37766  rrnequiv  37805  aks4d1p1p3  42028  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p5  42039  posbezout  42059  primrootlekpowne0  42064  aks6d1c5lem1  42095  2np3bcnp1  42103  sticksstones10  42114  sticksstones12a  42116  sticksstones22  42127  aks6d1c7lem1  42139  unitscyglem2  42155  metakunt1  42164  metakunt12  42175  metakunt28  42191  metakunt30  42193  flt4lem7  42629  fltnltalem  42632  fltnlta  42633  irrapxlem1  42792  pell14qrgapw  42846  monotoddzzfi  42913  ltrmynn0  42919  jm2.24nn  42930  acongeq  42954  jm2.26lem3  42972  jm3.1lem2  42989  binomcxplemnotnn0  44328  isosctrlem1ALT  44906  rfcnnnub  45008  zltlesub  45262  monoords  45274  supxrge  45313  infleinflem2  45346  uzubioo  45542  fmul01lt1lem1  45561  fmul01lt1lem2  45562  lptre2pt  45617  addlimc  45625  0ellimcdiv  45626  limclner  45628  climleltrp  45653  limsupubuzlem  45689  limsup10exlem  45749  icccncfext  45864  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnmul  45920  iblspltprt  45950  itgspltprt  45956  stoweidlem5  45982  stoweidlem11  45988  stoweidlem13  45990  stoweidlem14  45991  stoweidlem25  46002  stoweidlem26  46003  stoweidlem42  46019  stoweidlem59  46036  stoweid  46040  wallispilem3  46044  wallispilem4  46045  wallispilem5  46046  fourierdlem10  46094  fourierdlem11  46095  fourierdlem12  46096  fourierdlem15  46099  fourierdlem20  46104  fourierdlem24  46108  fourierdlem30  46114  fourierdlem31  46115  fourierdlem33  46117  fourierdlem40  46124  fourierdlem41  46125  fourierdlem42  46126  fourierdlem43  46127  fourierdlem44  46128  fourierdlem46  46129  fourierdlem47  46130  fourierdlem48  46131  fourierdlem50  46133  fourierdlem63  46146  fourierdlem64  46147  fourierdlem65  46148  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem77  46160  fourierdlem78  46161  fourierdlem79  46162  fourierdlem87  46170  fourierdlem91  46174  fourierdlem92  46175  fourierdlem103  46186  fourierdlem104  46187  fouriersw  46208  etransclem19  46230  etransclem23  46234  etransclem48  46259  ioorrnopnlem  46281  iundjiun  46437  omeiunltfirp  46496  caratheodorylem1  46503  hoicvr  46525  hoidmv1lelem2  46569  hoidmvlelem2  46573  hoiqssbllem2  46600  vonioolem1  46657  vonicclem1  46660  smflimlem4  46751  smfmullem1  46768  2tceilhalfelfzo1  47309  addmodne  47321  iccpartgt  47389  perfectALTVlem2  47684  bgoldbtbndlem2  47768  pgrple2abl  48288  logbpw2m1  48495  dignn0ldlem  48530  2itscp  48709