Theorem lelttrd 10798

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114   class class class wbr 5066  ℝcr 10536   < clt 10675   ≤ cle 10676

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-pre-lttri 10611  ax-pre-lttrn 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681

This theorem is referenced by:  lt2msq1  11524  suprzcl  12063  ge0p1rp  12421  elfzolt3  13049  flflp1  13178  ltdifltdiv  13205  modsubdir  13309  seqf1olem1  13410  seqf1olem2  13411  expmulnbnd  13597  discr1  13601  faclbnd5  13659  bcp1nk  13678  hashfun  13799  swrds2  14302  abslt  14674  abs3lem  14698  fzomaxdiflem  14702  icodiamlt  14795  reccn2  14953  o1rlimmul  14975  caucvgrlem  15029  geomulcvg  15232  mertenslem1  15240  bpoly4  15413  ef01bndlem  15537  sin01bnd  15538  cos01bnd  15539  sinltx  15542  eirrlem  15557  rpnnen2lem11  15577  ruclem10  15592  bitsfzolem  15783  bitsfzo  15784  bitsinv1lem  15790  smueqlem  15839  pcfaclem  16234  pockthg  16242  prmreclem5  16256  1arith  16263  4sqlem11  16291  4sqlem12  16292  4sqlem13  16293  coe1tmmul2  20444  ssblex  23038  nlmvscnlem2  23294  nlmvscnlem1  23295  nrginvrcnlem  23300  blcvx  23406  icccmplem2  23431  reconnlem2  23435  metdcnlem  23444  icopnfcnv  23546  nmoleub2lem3  23719  ipcnlem2  23847  ipcnlem1  23848  minveclem3b  24031  minveclem3  24032  pjthlem1  24040  pmltpclem2  24050  ivthlem2  24053  ovollb2lem  24089  iundisj  24149  uniioombllem3  24186  opnmbllem  24202  itg2monolem3  24353  itg2cnlem2  24363  dveflem  24576  dvferm2lem  24583  lhop1lem  24610  dvcnvre  24616  ftc1a  24634  ftc1lem4  24636  coeeulem  24814  dgradd2  24858  aaliou2b  24930  ulmdvlem1  24988  itgulm  24996  radcnvlem1  25001  radcnvlt1  25006  radcnvle  25008  psercnlem1  25013  pserdvlem1  25015  pserdv  25017  abelthlem2  25020  abelthlem7  25026  cosordlem  25115  tanord1  25121  efif1olem1  25126  logcnlem3  25227  logcnlem4  25228  efopnlem1  25239  logtayl  25243  cxpcn3lem  25328  birthdaylem3  25531  efrlim  25547  lgamgulmlem2  25607  lgamucov  25615  ftalem1  25650  ftalem2  25651  ftalem5  25654  basellem1  25658  basellem3  25660  perfectlem2  25806  bposlem1  25860  bposlem3  25862  bposlem6  25865  lgsdirprm  25907  lgsqrlem2  25923  lgseisen  25955  lgsquadlem1  25956  lgsquadlem2  25957  2sqlem8  26002  2sqblem  26007  dchrvmasumiflem1  26077  pntrmax  26140  pntlemc  26171  pntlemg  26174  pntlemr  26178  axpaschlem  26726  axlowdimlem16  26743  clwwisshclwwslem  27792  smcnlem  28474  minvecolem3  28653  pjhthlem1  29168  nmcexi  29803  iundisjf  30339  iundisjfi  30519  psgnfzto1stlem  30742  dya2icoseg  31535  reprgt  31892  hgt750lem  31922  tgoldbachgtde  31931  subfaclim  32435  bcprod  32970  dnicn  33831  unbdqndv2lem1  33848  unbdqndv2lem2  33849  knoppndvlem18  33868  poimirlem6  34913  poimirlem7  34914  poimirlem12  34919  poimirlem15  34922  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem23  34930  poimirlem24  34931  opnmbllem0  34943  mblfinlem3  34946  mblfinlem4  34947  ftc1cnnclem  34980  ftc1anclem7  34988  isbnd3  35077  cntotbnd  35089  rrnequiv  35128  fltnltalem  39294  fltnlta  39295  irrapxlem1  39439  pell14qrgapw  39493  monotoddzzfi  39559  ltrmynn0  39565  jm2.24nn  39576  acongeq  39600  jm2.26lem3  39618  jm3.1lem2  39635  binomcxplemnotnn0  40708  isosctrlem1ALT  41288  rfcnnnub  41313  zltlesub  41571  monoords  41584  supxrge  41626  infleinflem2  41659  uzubioo  41863  fmul01lt1lem1  41885  fmul01lt1lem2  41886  lptre2pt  41941  addlimc  41949  0ellimcdiv  41950  limclner  41952  climleltrp  41977  limsupubuzlem  42013  limsup10exlem  42073  icccncfext  42190  ioodvbdlimc1lem1  42236  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvnmul  42248  iblspltprt  42278  itgspltprt  42284  stoweidlem5  42310  stoweidlem11  42316  stoweidlem13  42318  stoweidlem14  42319  stoweidlem25  42330  stoweidlem26  42331  stoweidlem42  42347  stoweidlem59  42364  stoweid  42368  wallispilem3  42372  wallispilem4  42373  wallispilem5  42374  fourierdlem10  42422  fourierdlem11  42423  fourierdlem12  42424  fourierdlem15  42427  fourierdlem20  42432  fourierdlem24  42436  fourierdlem30  42442  fourierdlem31  42443  fourierdlem33  42445  fourierdlem40  42452  fourierdlem41  42453  fourierdlem42  42454  fourierdlem43  42455  fourierdlem44  42456  fourierdlem46  42457  fourierdlem47  42458  fourierdlem48  42459  fourierdlem50  42461  fourierdlem63  42474  fourierdlem64  42475  fourierdlem65  42476  fourierdlem73  42484  fourierdlem74  42485  fourierdlem75  42486  fourierdlem76  42487  fourierdlem77  42488  fourierdlem78  42489  fourierdlem79  42490  fourierdlem87  42498  fourierdlem91  42502  fourierdlem92  42503  fourierdlem103  42514  fourierdlem104  42515  fouriersw  42536  etransclem19  42558  etransclem23  42562  etransclem48  42587  ioorrnopnlem  42609  iundjiun  42762  omeiunltfirp  42821  caratheodorylem1  42828  hoicvr  42850  hoidmv1lelem2  42894  hoidmvlelem2  42898  hoiqssbllem2  42925  vonioolem1  42982  vonicclem1  42985  smflimlem4  43070  smfmullem1  43086  iccpartgt  43607  perfectALTVlem2  43907  bgoldbtbndlem2  43991  pgrple2abl  44433  logbpw2m1  44647  dignn0ldlem  44682  2itscp  44788