Theorem lelttrd 10536

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

Syntax hints:   → wi 4   ∧ wa 386   ∈ wcel 2107   class class class wbr 4888  ℝcr 10273   < clt 10413   ≤ cle 10414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5019  ax-nul 5027  ax-pow 5079  ax-pr 5140  ax-un 7228  ax-resscn 10331  ax-pre-lttri 10348  ax-pre-lttrn 10349

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4674  df-br 4889  df-opab 4951  df-mpt 4968  df-id 5263  df-xp 5363  df-rel 5364  df-cnv 5365  df-co 5366  df-dm 5367  df-rn 5368  df-res 5369  df-ima 5370  df-iota 6101  df-fun 6139  df-fn 6140  df-f 6141  df-f1 6142  df-fo 6143  df-f1o 6144  df-fv 6145  df-er 8028  df-en 8244  df-dom 8245  df-sdom 8246  df-pnf 10415  df-mnf 10416  df-xr 10417  df-ltxr 10418  df-le 10419

This theorem is referenced by:  lt2msq1  11263  suprzcl  11813  ge0p1rp  12174  elfzolt3  12803  flflp1  12931  ltdifltdiv  12958  modsubdir  13062  seqf1olem1  13162  seqf1olem2  13163  expmulnbnd  13319  discr1  13323  faclbnd5  13407  bcp1nk  13426  hashfun  13542  swrds2  14095  abslt  14465  abs3lem  14489  fzomaxdiflem  14493  icodiamlt  14586  reccn2  14739  o1rlimmul  14761  caucvgrlem  14815  geomulcvg  15015  mertenslem1  15023  bpoly4  15196  ef01bndlem  15320  sin01bnd  15321  cos01bnd  15322  sinltx  15325  eirrlem  15340  rpnnen2lem11  15361  ruclem10  15376  bitsfzolem  15566  bitsfzo  15567  bitsinv1lem  15573  smueqlem  15622  pcfaclem  16010  pockthg  16018  prmreclem5  16032  1arith  16039  4sqlem11  16067  4sqlem12  16068  4sqlem13  16069  coe1tmmul2  20046  ssblex  22645  nlmvscnlem2  22901  nlmvscnlem1  22902  nrginvrcnlem  22907  blcvx  23013  icccmplem2  23038  reconnlem2  23042  metdcnlem  23051  icopnfcnv  23153  nmoleub2lem3  23326  ipcnlem2  23454  ipcnlem1  23455  minveclem3b  23638  minveclem3  23639  pjthlem1  23647  pmltpclem2  23657  ivthlem2  23660  ovollb2lem  23696  iundisj  23756  uniioombllem3  23793  opnmbllem  23809  itg2monolem3  23960  itg2cnlem2  23970  dveflem  24183  dvferm2lem  24190  lhop1lem  24217  dvcnvre  24223  ftc1a  24241  ftc1lem4  24243  coeeulem  24421  dgradd2  24465  aaliou2b  24537  ulmdvlem1  24595  itgulm  24603  radcnvlem1  24608  radcnvlt1  24613  radcnvle  24615  psercnlem1  24620  pserdvlem1  24622  pserdv  24624  abelthlem2  24627  abelthlem7  24633  cosordlem  24719  tanord1  24725  efif1olem1  24730  logcnlem3  24831  logcnlem4  24832  efopnlem1  24843  logtayl  24847  cxpcn3lem  24932  birthdaylem3  25136  efrlim  25152  lgamgulmlem2  25212  lgamucov  25220  ftalem1  25255  ftalem2  25256  ftalem5  25259  basellem1  25263  basellem3  25265  perfectlem2  25411  bposlem1  25465  bposlem3  25467  bposlem6  25470  lgsdirprm  25512  lgsqrlem2  25528  lgseisen  25560  lgsquadlem1  25561  lgsquadlem2  25562  2sqlem8  25607  2sqblem  25612  dchrvmasumiflem1  25646  pntrmax  25709  pntlemc  25740  pntlemg  25743  pntlemr  25747  axpaschlem  26293  axlowdimlem16  26310  clwwisshclwwslem  27407  smcnlem  28128  minvecolem3  28308  pjhthlem1  28826  nmcexi  29461  iundisjf  29969  iundisjfi  30123  psgnfzto1stlem  30452  dya2icoseg  30941  reprgt  31305  hgt750lem  31335  tgoldbachgtde  31344  subfaclim  31773  bcprod  32222  dnicn  33069  unbdqndv2lem1  33086  unbdqndv2lem2  33087  knoppndvlem18  33106  poimirlem6  34046  poimirlem7  34047  poimirlem12  34052  poimirlem15  34055  poimirlem17  34057  poimirlem19  34059  poimirlem20  34060  poimirlem23  34063  poimirlem24  34064  opnmbllem0  34076  mblfinlem3  34079  mblfinlem4  34080  ftc1cnnclem  34113  ftc1anclem7  34121  isbnd3  34212  cntotbnd  34224  rrnequiv  34263  irrapxlem1  38356  pell14qrgapw  38410  monotoddzzfi  38476  ltrmynn0  38484  jm2.24nn  38495  acongeq  38519  jm2.26lem3  38537  jm3.1lem2  38554  binomcxplemnotnn0  39521  isosctrlem1ALT  40113  rfcnnnub  40138  zltlesub  40417  monoords  40430  supxrge  40472  infleinflem2  40505  uzubioo  40712  fmul01lt1lem1  40734  fmul01lt1lem2  40735  lptre2pt  40790  addlimc  40798  0ellimcdiv  40799  limclner  40801  climleltrp  40826  limsupubuzlem  40862  limsup10exlem  40922  icccncfext  41038  ioodvbdlimc1lem1  41084  ioodvbdlimc1lem2  41085  ioodvbdlimc2lem  41087  dvnmul  41096  iblspltprt  41126  itgspltprt  41132  stoweidlem5  41159  stoweidlem11  41165  stoweidlem13  41167  stoweidlem14  41168  stoweidlem25  41179  stoweidlem26  41180  stoweidlem42  41196  stoweidlem59  41213  stoweid  41217  wallispilem3  41221  wallispilem4  41222  wallispilem5  41223  fourierdlem10  41271  fourierdlem11  41272  fourierdlem12  41273  fourierdlem15  41276  fourierdlem20  41281  fourierdlem24  41285  fourierdlem30  41291  fourierdlem31  41292  fourierdlem33  41294  fourierdlem40  41301  fourierdlem41  41302  fourierdlem42  41303  fourierdlem43  41304  fourierdlem44  41305  fourierdlem46  41306  fourierdlem47  41307  fourierdlem48  41308  fourierdlem50  41310  fourierdlem63  41323  fourierdlem64  41324  fourierdlem65  41325  fourierdlem73  41333  fourierdlem74  41334  fourierdlem75  41335  fourierdlem76  41336  fourierdlem77  41337  fourierdlem78  41338  fourierdlem79  41339  fourierdlem87  41347  fourierdlem91  41351  fourierdlem92  41352  fourierdlem103  41363  fourierdlem104  41364  fouriersw  41385  etransclem19  41407  etransclem23  41411  etransclem48  41436  ioorrnopnlem  41458  iundjiun  41611  omeiunltfirp  41670  caratheodorylem1  41677  hoicvr  41699  hoidmv1lelem2  41743  hoidmvlelem2  41747  hoiqssbllem2  41774  vonioolem1  41831  vonicclem1  41834  smflimlem4  41919  smfmullem1  41935  iccpartgt  42405  perfectALTVlem2  42666  bgoldbtbndlem2  42729  pgrple2abl  43171  logbpw2m1  43386  dignn0ldlem  43421  2itscp  43527