Theorem lelttrd 11293

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   class class class wbr 5098  ℝcr 11027   < clt 11168   ≤ cle 11169

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pow 5310  ax-pr 5377  ax-un 7680  ax-resscn 11085  ax-pre-lttri 11102  ax-pre-lttrn 11103

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8635  df-en 8886  df-dom 8887  df-sdom 8888  df-pnf 11170  df-mnf 11171  df-xr 11172  df-ltxr 11173  df-le 11174

This theorem is referenced by:  lt2msq1  12028  suprzcl  12574  ge0p1rp  12940  elfzolt3  13587  flflp1  13729  ltdifltdiv  13756  modsubdir  13865  seqf1olem1  13966  seqf1olem2  13967  expmulnbnd  14160  discr1  14164  faclbnd5  14223  bcp1nk  14242  hashfun  14362  swrds2  14865  abslt  15240  abs3lem  15264  fzomaxdiflem  15268  icodiamlt  15363  reccn2  15522  o1rlimmul  15544  caucvgrlem  15598  geomulcvg  15801  mertenslem1  15809  bpoly4  15984  ef01bndlem  16111  sin01bnd  16112  cos01bnd  16113  sinltx  16116  eirrlem  16131  rpnnen2lem11  16151  ruclem10  16166  bitsfzolem  16363  bitsfzo  16364  bitsinv1lem  16370  smueqlem  16419  pcfaclem  16828  pockthg  16836  prmreclem5  16850  1arith  16857  4sqlem11  16885  4sqlem12  16886  4sqlem13  16887  coe1tmmul2  22220  ssblex  24374  nlmvscnlem2  24631  nlmvscnlem1  24632  nrginvrcnlem  24637  blcvx  24744  icccmplem2  24770  reconnlem2  24774  metdcnlem  24783  icopnfcnv  24898  nmoleub2lem3  25073  ipcnlem2  25202  ipcnlem1  25203  minveclem3b  25386  minveclem3  25387  pjthlem1  25395  pmltpclem2  25408  ivthlem2  25411  ovollb2lem  25447  iundisj  25507  uniioombllem3  25544  opnmbllem  25560  itg2monolem3  25711  itg2cnlem2  25721  dveflem  25941  dvferm2lem  25948  lhop1lem  25976  dvcnvre  25982  ftc1a  26002  ftc1lem4  26004  coeeulem  26187  dgradd2  26232  aaliou2b  26307  ulmdvlem1  26367  itgulm  26375  radcnvlem1  26380  radcnvlt1  26385  radcnvle  26387  psercnlem1  26393  pserdvlem1  26395  pserdv  26397  abelthlem2  26400  abelthlem7  26406  cosordlem  26497  tanord1  26504  efif1olem1  26509  logcnlem3  26611  logcnlem4  26612  efopnlem1  26623  logtayl  26627  cxpcn3lem  26715  birthdaylem3  26921  efrlim  26937  efrlimOLD  26938  lgamgulmlem2  26998  lgamucov  27006  ftalem1  27041  ftalem2  27042  ftalem5  27045  basellem1  27049  basellem3  27051  perfectlem2  27199  bposlem1  27253  bposlem3  27255  bposlem6  27258  lgsdirprm  27300  lgsqrlem2  27316  lgseisen  27348  lgsquadlem1  27349  lgsquadlem2  27350  2sqlem8  27395  2sqblem  27400  dchrvmasumiflem1  27470  pntrmax  27533  pntlemc  27564  pntlemg  27567  pntlemr  27571  axpaschlem  29015  axlowdimlem16  29032  clwwisshclwwslem  30091  smcnlem  30774  minvecolem3  30953  pjhthlem1  31468  nmcexi  32103  iundisjf  32666  iundisjfi  32878  psgnfzto1stlem  33184  esplyfval2  33725  esplyfval3  33732  cos9thpiminplylem1  33941  dya2icoseg  34436  reprgt  34780  hgt750lem  34810  tgoldbachgtde  34819  subfaclim  35384  bcprod  35934  dnicn  36694  unbdqndv2lem1  36711  unbdqndv2lem2  36712  knoppndvlem18  36731  poimirlem6  37829  poimirlem7  37830  poimirlem12  37835  poimirlem15  37838  poimirlem17  37840  poimirlem19  37842  poimirlem20  37843  poimirlem23  37846  poimirlem24  37847  opnmbllem0  37859  mblfinlem3  37862  mblfinlem4  37863  ftc1cnnclem  37894  ftc1anclem7  37902  isbnd3  37987  cntotbnd  37999  rrnequiv  38038  aks4d1p1p3  42345  aks4d1p1p2  42346  aks4d1p1p4  42347  aks4d1p1p7  42350  aks4d1p1p5  42351  aks4d1p5  42356  posbezout  42376  primrootlekpowne0  42381  aks6d1c5lem1  42412  2np3bcnp1  42420  sticksstones10  42431  sticksstones12a  42433  sticksstones22  42444  aks6d1c7lem1  42456  unitscyglem2  42472  flt4lem7  42923  fltnltalem  42926  fltnlta  42927  irrapxlem1  43085  pell14qrgapw  43139  monotoddzzfi  43205  ltrmynn0  43211  jm2.24nn  43222  acongeq  43246  jm2.26lem3  43264  jm3.1lem2  43281  binomcxplemnotnn0  44618  isosctrlem1ALT  45195  rfcnnnub  45302  zltlesub  45554  monoords  45566  supxrge  45604  infleinflem2  45636  uzubioo  45832  fmul01lt1lem1  45851  fmul01lt1lem2  45852  lptre2pt  45905  addlimc  45913  0ellimcdiv  45914  limclner  45916  climleltrp  45941  limsupubuzlem  45977  limsup10exlem  46037  icccncfext  46152  ioodvbdlimc1lem1  46196  ioodvbdlimc1lem2  46197  ioodvbdlimc2lem  46199  dvnmul  46208  iblspltprt  46238  itgspltprt  46244  stoweidlem5  46270  stoweidlem11  46276  stoweidlem13  46278  stoweidlem14  46279  stoweidlem25  46290  stoweidlem26  46291  stoweidlem42  46307  stoweidlem59  46324  stoweid  46328  wallispilem3  46332  wallispilem4  46333  wallispilem5  46334  fourierdlem10  46382  fourierdlem11  46383  fourierdlem12  46384  fourierdlem15  46387  fourierdlem20  46392  fourierdlem24  46396  fourierdlem30  46402  fourierdlem31  46403  fourierdlem33  46405  fourierdlem40  46412  fourierdlem41  46413  fourierdlem42  46414  fourierdlem43  46415  fourierdlem44  46416  fourierdlem46  46417  fourierdlem47  46418  fourierdlem48  46419  fourierdlem50  46421  fourierdlem63  46434  fourierdlem64  46435  fourierdlem65  46436  fourierdlem73  46444  fourierdlem74  46445  fourierdlem75  46446  fourierdlem76  46447  fourierdlem77  46448  fourierdlem78  46449  fourierdlem79  46450  fourierdlem87  46458  fourierdlem91  46462  fourierdlem92  46463  fourierdlem103  46474  fourierdlem104  46475  fouriersw  46496  etransclem19  46518  etransclem23  46522  etransclem48  46547  ioorrnopnlem  46569  iundjiun  46725  omeiunltfirp  46784  caratheodorylem1  46791  hoicvr  46813  hoidmv1lelem2  46857  hoidmvlelem2  46861  hoiqssbllem2  46888  vonioolem1  46945  vonicclem1  46948  smflimlem4  47039  smfmullem1  47056  2tceilhalfelfzo1  47599  addmodne  47611  iccpartgt  47694  perfectALTVlem2  47989  bgoldbtbndlem2  48073  pgrple2abl  48632  logbpw2m1  48834  dignn0ldlem  48869  2itscp  49048