Theorem lelttrd 11298

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ℝcr 11031   < clt 11173   ≤ cle 11174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-pre-lttri 11106  ax-pre-lttrn 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179

This theorem is referenced by:  lt2msq1  12034  suprzcl  12603  ge0p1rp  12969  elfzolt3  13618  flflp1  13760  ltdifltdiv  13787  modsubdir  13896  seqf1olem1  13997  seqf1olem2  13998  expmulnbnd  14191  discr1  14195  faclbnd5  14254  bcp1nk  14273  hashfun  14393  swrds2  14896  abslt  15271  abs3lem  15295  fzomaxdiflem  15299  icodiamlt  15394  reccn2  15553  o1rlimmul  15575  caucvgrlem  15629  geomulcvg  15835  mertenslem1  15843  bpoly4  16018  ef01bndlem  16145  sin01bnd  16146  cos01bnd  16147  sinltx  16150  eirrlem  16165  rpnnen2lem11  16185  ruclem10  16200  bitsfzolem  16397  bitsfzo  16398  bitsinv1lem  16404  smueqlem  16453  pcfaclem  16863  pockthg  16871  prmreclem5  16885  1arith  16892  4sqlem11  16920  4sqlem12  16921  4sqlem13  16922  coe1tmmul2  22254  ssblex  24406  nlmvscnlem2  24663  nlmvscnlem1  24664  nrginvrcnlem  24669  blcvx  24776  icccmplem2  24802  reconnlem2  24806  metdcnlem  24815  icopnfcnv  24922  nmoleub2lem3  25095  ipcnlem2  25224  ipcnlem1  25225  minveclem3b  25408  minveclem3  25409  pjthlem1  25417  pmltpclem2  25429  ivthlem2  25432  ovollb2lem  25468  iundisj  25528  uniioombllem3  25565  opnmbllem  25581  itg2monolem3  25732  itg2cnlem2  25742  dveflem  25959  dvferm2lem  25966  lhop1lem  25993  dvcnvre  25999  ftc1a  26017  ftc1lem4  26019  coeeulem  26202  dgradd2  26246  aaliou2b  26321  ulmdvlem1  26381  itgulm  26389  radcnvlem1  26394  radcnvlt1  26399  radcnvle  26401  psercnlem1  26406  pserdvlem1  26408  pserdv  26410  abelthlem2  26413  abelthlem7  26419  cosordlem  26510  tanord1  26517  efif1olem1  26522  logcnlem3  26624  logcnlem4  26625  efopnlem1  26636  logtayl  26640  cxpcn3lem  26727  birthdaylem3  26933  efrlim  26949  efrlimOLD  26950  lgamgulmlem2  27010  lgamucov  27018  ftalem1  27053  ftalem2  27054  ftalem5  27057  basellem1  27061  basellem3  27063  perfectlem2  27210  bposlem1  27264  bposlem3  27266  bposlem6  27269  lgsdirprm  27311  lgsqrlem2  27327  lgseisen  27359  lgsquadlem1  27360  lgsquadlem2  27361  2sqlem8  27406  2sqblem  27411  dchrvmasumiflem1  27481  pntrmax  27544  pntlemc  27575  pntlemg  27578  pntlemr  27582  axpaschlem  29026  axlowdimlem16  29043  clwwisshclwwslem  30102  smcnlem  30786  minvecolem3  30965  pjhthlem1  31480  nmcexi  32115  iundisjf  32677  iundisjfi  32887  psgnfzto1stlem  33179  esplyfval2  33727  esplyfval3  33734  cos9thpiminplylem1  33945  dya2icoseg  34440  reprgt  34784  hgt750lem  34814  tgoldbachgtde  34823  subfaclim  35389  bcprod  35939  dnicn  36771  unbdqndv2lem1  36788  unbdqndv2lem2  36789  knoppndvlem18  36808  poimirlem6  37964  poimirlem7  37965  poimirlem12  37970  poimirlem15  37973  poimirlem17  37975  poimirlem19  37977  poimirlem20  37978  poimirlem23  37981  poimirlem24  37982  opnmbllem0  37994  mblfinlem3  37997  mblfinlem4  37998  ftc1cnnclem  38029  ftc1anclem7  38037  isbnd3  38122  cntotbnd  38134  rrnequiv  38173  aks4d1p1p3  42525  aks4d1p1p2  42526  aks4d1p1p4  42527  aks4d1p1p7  42530  aks4d1p1p5  42531  aks4d1p5  42536  posbezout  42556  primrootlekpowne0  42561  aks6d1c5lem1  42592  2np3bcnp1  42600  sticksstones10  42611  sticksstones12a  42613  sticksstones22  42624  aks6d1c7lem1  42636  unitscyglem2  42652  flt4lem7  43109  fltnltalem  43112  fltnlta  43113  irrapxlem1  43271  pell14qrgapw  43325  monotoddzzfi  43391  ltrmynn0  43397  jm2.24nn  43408  acongeq  43432  jm2.26lem3  43450  jm3.1lem2  43467  binomcxplemnotnn0  44804  isosctrlem1ALT  45381  rfcnnnub  45488  zltlesub  45739  monoords  45751  supxrge  45789  infleinflem2  45821  uzubioo  46016  fmul01lt1lem1  46035  fmul01lt1lem2  46036  lptre2pt  46089  addlimc  46097  0ellimcdiv  46098  limclner  46100  climleltrp  46125  limsupubuzlem  46161  limsup10exlem  46221  icccncfext  46336  ioodvbdlimc1lem1  46380  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnmul  46392  iblspltprt  46422  itgspltprt  46428  stoweidlem5  46454  stoweidlem11  46460  stoweidlem13  46462  stoweidlem14  46463  stoweidlem25  46474  stoweidlem26  46475  stoweidlem42  46491  stoweidlem59  46508  stoweid  46512  wallispilem3  46516  wallispilem4  46517  wallispilem5  46518  fourierdlem10  46566  fourierdlem11  46567  fourierdlem12  46568  fourierdlem15  46571  fourierdlem20  46576  fourierdlem24  46580  fourierdlem30  46586  fourierdlem31  46587  fourierdlem33  46589  fourierdlem40  46596  fourierdlem41  46597  fourierdlem42  46598  fourierdlem43  46599  fourierdlem44  46600  fourierdlem46  46601  fourierdlem47  46602  fourierdlem48  46603  fourierdlem50  46605  fourierdlem63  46618  fourierdlem64  46619  fourierdlem65  46620  fourierdlem73  46628  fourierdlem74  46629  fourierdlem75  46630  fourierdlem76  46631  fourierdlem77  46632  fourierdlem78  46633  fourierdlem79  46634  fourierdlem87  46642  fourierdlem91  46646  fourierdlem92  46647  fourierdlem103  46658  fourierdlem104  46659  fouriersw  46680  etransclem19  46702  etransclem23  46706  etransclem48  46731  ioorrnopnlem  46753  iundjiun  46909  omeiunltfirp  46968  caratheodorylem1  46975  hoicvr  46997  hoidmv1lelem2  47041  hoidmvlelem2  47045  hoiqssbllem2  47072  vonioolem1  47129  vonicclem1  47132  smflimlem4  47223  smfmullem1  47240  2tceilhalfelfzo1  47799  addmodne  47813  2timesltsqm1  47842  iccpartgt  47902  perfectALTVlem2  48213  bgoldbtbndlem2  48297  pgrple2abl  48856  logbpw2m1  49058  dignn0ldlem  49093  2itscp  49272