Theorem lelttrd 11385

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 11317	. . 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 2146   class class class wbr 5111  ℝcr 11116   < clt 11260   ≤ cle 11261

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11174  ax-pre-lttri 11191  ax-pre-lttrn 11192

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 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266

This theorem is used by:  lt2msq1  12116  suprzcl  12694  ge0p1rp  13067  elfzolt3  13717  flflp1  13860  ltdifltdiv  13887  modsubdir  13996  seqf1olem1  14097  seqf1olem2  14098  expmulnbnd  14291  discr1  14295  faclbnd5  14354  bcp1nk  14373  hashfun  14494  swrds2  15003  abslt  15392  abs3lem  15416  fzomaxdiflem  15420  icodiamlt  15515  reccn2  15674  o1rlimmul  15696  caucvgrlem  15750  geomulcvg  15955  mertenslem1  15963  bpoly4  16137  ef01bndlem  16264  sin01bnd  16265  cos01bnd  16266  sinltx  16269  eirrlem  16284  rpnnen2lem11  16304  ruclem10  16319  bitsfzolem  16516  bitsfzo  16517  bitsinv1lem  16523  smueqlem  16572  pcfaclem  16982  pockthg  16990  prmreclem5  17004  1arith  17011  4sqlem11  17039  4sqlem12  17040  4sqlem13  17041  coe1tmmul2  22489  ssblex  24638  nlmvscnlem2  24895  nlmvscnlem1  24896  nrginvrcnlem  24901  blcvx  25008  icccmplem2  25034  reconnlem2  25038  metdcnlem  25047  icopnfcnv  25154  nmoleub2lem3  25327  ipcnlem2  25456  ipcnlem1  25457  minveclem3b  25640  minveclem3  25641  pjthlem1  25649  pmltpclem2  25661  ivthlem2  25664  ovollb2lem  25700  iundisj  25760  uniioombllem3  25797  opnmbllem  25813  itg2monolem3  25964  itg2cnlem2  25974  dveflem  26191  dvferm2lem  26198  lhop1lem  26225  dvcnvre  26231  ftc1a  26249  ftc1lem4  26251  coeeulem  26434  dgradd2  26478  aaliou2b  26557  ulmdvlem1  26616  itgulm  26624  radcnvlem1  26629  radcnvlt1  26634  radcnvle  26636  psercnlem1  26641  pserdvlem1  26643  pserdv  26645  abelthlem2  26648  abelthlem7  26654  cosordlem  26748  tanord1  26755  efif1olem1  26760  logcnlem3  26862  logcnlem4  26863  efopnlem1  26874  logtayl  26878  cxpcn3lem  26965  birthdaylem3  27171  efrlim  27187  lgamgulmlem2  27247  lgamucov  27255  ftalem1  27290  ftalem2  27291  ftalem5  27294  basellem1  27298  basellem3  27300  perfectlem2  27447  bposlem1  27501  bposlem3  27503  bposlem6  27506  lgsdirprm  27548  lgsqrlem2  27564  lgseisen  27596  lgsquadlem1  27597  lgsquadlem2  27598  2sqlem8  27643  2sqblem  27648  dchrvmasumiflem1  27718  pntrmax  27781  pntlemc  27812  pntlemg  27815  pntlemr  27819  axpaschlem  29347  axlowdimlem16  29364  clwwisshclwwslem  30434  smcnlem  31122  minvecolem3  31301  pjhthlem1  31816  nmcexi  32451  iundisjf  33007  iundisjfi  33213  psgnfzto1stlem  33486  esplyfval2  34021  esplyfval3  34028  cos9thpiminplylem1  34238  dya2icoseg  34734  reprgt  35075  hgt750lem  35105  tgoldbachgtde  35114  subfaclim  35719  bcprod  36269  dnicn  37140  unbdqndv2lem1  37157  unbdqndv2lem2  37158  knoppndvlem18  37177  poimirlem6  38336  poimirlem7  38337  poimirlem12  38342  poimirlem15  38345  poimirlem17  38347  poimirlem19  38349  poimirlem20  38350  poimirlem23  38353  poimirlem24  38354  opnmbllem0  38366  mblfinlem3  38369  mblfinlem4  38370  ftc1cnnclem  38401  ftc1anclem7  38409  isbnd3  38495  cntotbnd  38507  rrnequiv  38546  aks4d1p1p3  42896  aks4d1p1p2  42897  aks4d1p1p4  42898  aks4d1p1p7  42901  aks4d1p1p5  42902  aks4d1p5  42907  posbezout  42927  primrootlekpowne0  42932  aks6d1c5lem1  42963  2np3bcnp1  42971  sticksstones10  42982  sticksstones12a  42984  sticksstones22  42995  aks6d1c7lem1  43007  unitscyglem2  43023  flt4lem7  43451  fltnltalem  43454  fltnlta  43455  irrapxlem1  43609  pell14qrgapw  43663  monotoddzzfi  43729  ltrmynn0  43735  jm2.24nn  43746  acongeq  43770  jm2.26lem3  43788  jm3.1lem2  43805  binomcxplemnotnn0  45126  isosctrlem1ALT  45702  rfcnnnub  45816  zltlesub  46064  monoords  46076  supxrge  46114  infleinflem2  46146  uzubioo  46341  fmul01lt1lem1  46360  fmul01lt1lem2  46361  lptre2pt  46414  addlimc  46422  0ellimcdiv  46423  limclner  46425  climleltrp  46450  limsupubuzlem  46486  limsup10exlem  46546  icccncfext  46661  ioodvbdlimc1lem1  46705  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  dvnmul  46717  iblspltprt  46747  itgspltprt  46753  stoweidlem5  46779  stoweidlem11  46785  stoweidlem13  46787  stoweidlem14  46788  stoweidlem25  46799  stoweidlem26  46800  stoweidlem42  46816  stoweidlem59  46833  stoweid  46837  wallispilem3  46841  wallispilem4  46842  wallispilem5  46843  fourierdlem10  46891  fourierdlem11  46892  fourierdlem12  46893  fourierdlem15  46896  fourierdlem20  46901  fourierdlem24  46905  fourierdlem30  46911  fourierdlem31  46912  fourierdlem33  46914  fourierdlem40  46921  fourierdlem41  46922  fourierdlem42  46923  fourierdlem43  46924  fourierdlem44  46925  fourierdlem46  46926  fourierdlem47  46927  fourierdlem48  46928  fourierdlem50  46930  fourierdlem63  46943  fourierdlem64  46944  fourierdlem65  46945  fourierdlem73  46953  fourierdlem74  46954  fourierdlem75  46955  fourierdlem76  46956  fourierdlem77  46957  fourierdlem78  46958  fourierdlem79  46959  fourierdlem87  46967  fourierdlem91  46971  fourierdlem92  46972  fourierdlem103  46983  fourierdlem104  46984  fouriersw  47005  etransclem19  47027  etransclem23  47031  etransclem48  47056  ioorrnopnlem  47078  iundjiun  47234  omeiunltfirp  47293  caratheodorylem1  47300  hoicvr  47322  hoidmv1lelem2  47366  hoidmvlelem2  47370  hoiqssbllem2  47397  vonioolem1  47454  vonicclem1  47457  smflimlem4  47548  smfmullem1  47565  2tceilhalfelfzo1  48133  addmodne  48147  2timesltsqm1  48176  iccpartgt  48236  perfectALTVlem2  48547  bgoldbtbndlem2  48631  pgrple2abl  49204  logbpw2m1  49406  dignn0ldlem  49441  2itscp  49620