Theorem ltletrd 11394

Description: Transitive law deduction for 'less than', 'less than or equal to'. (Contributed by NM, 9-Jan-2006.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
letrd.3	⊢ (𝜑 → 𝐶 ∈ ℝ)
ltletrd.4	⊢ (𝜑 → 𝐴 < 𝐵)
ltletrd.5	⊢ (𝜑 → 𝐵 ≤ 𝐶)

Assertion

Ref	Expression
ltletrd	⊢ (𝜑 → 𝐴 < 𝐶)

Proof of Theorem ltletrd

Step	Hyp	Ref	Expression
1		ltletrd.4	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
2		ltletrd.5	. 2 ⊢ (𝜑 → 𝐵 ≤ 𝐶)
3		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		letrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		ltletr 11326	. . 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 2145   class class class wbr 5103  ℝcr 11123   < clt 11267   ≤ cle 11268

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-pre-lttri 11198  ax-pre-lttrn 11199

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273

This theorem is used by:  lelttrdi  11396  uzwo3  12992  rpgecl  13072  fznatpl1  13633  modabs  13965  seqf1olem1  14105  expgt1  14164  leexp2a  14236  bernneq3  14295  expnbnd  14296  expmulnbnd  14299  digit1  14301  discr1  14303  hashfun  14502  seqcoll2  14530  abssubne0  15404  icodiamlt  15525  reccn2  15684  isercolllem1  15752  isumltss  15937  fprodntriv  16029  efcllem  16163  sin01bnd  16273  cos01bnd  16274  sin01gt0  16278  eirrlem  16292  rpnnen2lem11  16312  ruclem10  16327  bitsmod  16526  bitsinv1lem  16531  smuval2  16572  prmreclem5  17012  1arith  17019  2expltfac  17184  mndodconglem  19668  sylow1lem1  19725  gzrngunit  21646  nlmvscnlem1  24912  nrginvrcnlem  24917  iccpnfhmeo  25173  cnheibor  25183  evth  25187  lebnumlem1  25189  ipcnlem1  25473  lmnn  25491  ovolicc2lem2  25746  itg2monolem1  25978  itg2monolem3  25980  dvferm1lem  26211  dvcnvre  26246  dvfsumlem3  26255  dvfsumrlim  26258  plyco0  26417  aaliou2b  26577  pilem2  26688  cosq34lt1  26764  cosordlem  26767  logdivlti  26857  logdivle  26859  logcnlem3  26881  logcnlem4  26882  cxpcn3lem  26984  atanre  27122  atanlogaddlem  27150  atans2  27168  birthdaylem3  27190  cxp2lim  27213  cxploglim2  27215  jensenlem2  27224  harmonicubnd  27246  fsumharmonic  27248  lgamgulmlem2  27266  lgamgulmlem3  27267  lgamucov  27274  ftalem2  27310  ftalem5  27313  vma1  27402  chtrpcl  27411  ppiltx  27413  fsumfldivdiaglem  27425  chtub  27448  fsumvma2  27450  chpval2  27454  chpchtsum  27455  chpub  27456  bpos1  27519  bposlem1  27520  bposlem2  27521  bposlem6  27525  gausslemma2dlem0c  27594  lgsquadlem1  27616  chebbnd1lem1  27705  chebbnd1lem2  27706  chebbnd1lem3  27707  chebbnd1  27708  chtppilimlem1  27709  chtppilimlem2  27710  chtppilim  27711  chto1ub  27712  chebbnd2  27713  chto1lb  27714  chpchtlim  27715  chpo1ub  27716  rplogsumlem2  27721  dchrisumlema  27724  dchrisumlem3  27727  dchrmusumlema  27729  dchrvmasumlem2  27734  dchrvmasumiflem1  27737  dchrisum0lema  27750  mulog2sumlem1  27770  chpdifbndlem1  27789  chpdifbnd  27791  pntrsumo1  27801  pntpbnd1  27822  pntpbnd2  27823  pntibndlem2  27827  pntlemb  27833  pntlemh  27835  pntlemr  27838  pntlem3  27845  pnt2  27849  ostth2lem1  27854  ostth2lem3  27871  ostth2lem4  27872  axsegconlem7  29380  axsegconlem10  29383  axlowdimlem16  29414  axcontlem2  29422  axcontlem4  29424  axcontlem7  29427  clwlkclwwlklem2a2  30463  clwwlkext2edg  30526  smatrcl  34306  1smat1  34314  lmdvg  34463  dya2icoseg  34788  eulerpartlems  34871  reprlt  35127  reprinfz1  35130  breprexplemc  35140  hgt750lemd  35156  hgt750lem  35159  hgt750leme  35166  tgoldbachgtde  35168  subfacval3  35768  knoppndvlem1  37209  knoppndvlem2  37210  knoppndvlem7  37215  knoppndvlem14  37222  knoppndvlem18  37226  poimirlem7  38376  poimirlem24  38393  poimirlem29  38398  mblfinlem2  38407  itg2addnclem  38420  itg2addnclem3  38422  ftc1anclem5  38446  ftc1anclem7  38448  ftc1anc  38450  areacirclem5  38461  lcmineqlem23  42917  3lexlogpow5ineq2  42921  3lexlogpow5ineq4  42922  3lexlogpow5ineq3  42923  aks4d1lem1  42928  dvrelog2  42930  aks4d1p1p3  42935  aks4d1p1p2  42936  aks4d1p1p4  42937  aks4d1p1p6  42939  aks4d1p1p7  42940  aks4d1p1p5  42941  aks4d1p1  42942  aks4d1p2  42943  aks4d1p3  42944  aks4d1p5  42946  aks4d1p6  42947  aks4d1p7d1  42948  aks4d1p7  42949  aks4d1p8d2  42951  aks4d1p8  42953  aks4d1p9  42954  posbezout  42966  hashscontpow1  42987  aks6d1c3  42989  2ap1caineq  43011  sticksstones12a  43023  sticksstones22  43034  aks6d1c7lem1  43046  aks6d1c7lem2  43047  aks6d1c7  43050  aks5lem6  43058  aks5lem8  43067  flt4lem7  43505  3cubeslem1  43529  irrapxlem4  43666  irrapxlem5  43667  pellexlem2  43671  pell14qrgapw  43717  pellqrex  43720  pellfundgt1  43724  pellfundex  43727  ltrmxnn0  43790  jm2.24nn  43800  jm2.17c  43803  jm2.24  43804  jm2.23  43837  jm3.1lem1  43858  jm3.1lem2  43859  radcnvrat  45138  dstregt0  46115  monoords  46130  uzubioo  46395  fsumnncl  46402  mullimc  46446  mullimcf  46453  sumnnodd  46460  limcleqr  46472  addlimc  46476  0ellimcdiv  46477  limclner  46479  limsupgtlem  46605  dvdivbd  46751  ioodvbdlimc1lem1  46759  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvnmul  46771  iblspltprt  46801  itgspltprt  46807  stoweidlem11  46839  stoweidlem24  46852  stoweidlem25  46853  stoweidlem26  46854  stoweidlem34  46862  stoweidlem36  46864  stoweidlem42  46870  stoweidlem44  46872  stoweidlem51  46879  stoweidlem59  46887  wallispi  46898  wallispi2lem1  46899  wallispi2  46901  stirlinglem11  46912  dirkertrigeqlem1  46926  dirkeritg  46930  fourierdlem10  46945  fourierdlem11  46946  fourierdlem12  46947  fourierdlem15  46950  fourierdlem19  46954  fourierdlem20  46955  fourierdlem30  46965  fourierdlem32  46967  fourierdlem40  46975  fourierdlem41  46976  fourierdlem44  46979  fourierdlem46  46980  fourierdlem47  46981  fourierdlem48  46982  fourierdlem49  46983  fourierdlem50  46984  fourierdlem63  46997  fourierdlem64  46998  fourierdlem65  46999  fourierdlem74  47008  fourierdlem75  47009  fourierdlem76  47010  fourierdlem78  47012  fourierdlem79  47013  fourierdlem89  47023  fourierdlem92  47026  fourierdlem103  47037  fourierdlem104  47038  fouriersw  47059  etransclem4  47066  etransclem23  47085  etransclem31  47093  etransclem32  47094  etransclem35  47097  etransclem41  47103  etransclem48  47110  ioorrnopnlem  47132  sge0uzfsumgt  47272  sge0seq  47274  iundjiun  47288  carageniuncllem2  47350  hoidmvlelem3  47425  iunhoiioolem  47503  vonioolem1  47508  smfmullem1  47619  smfmullem2  47620  smfmullem3  47621  ceilhalfgt1  48221  modm2nep1  48260  modp2nep1  48261  modm1nep2  48262  modm1nem2  48263  modm1p1ne  48264  bgoldbtbndlem2  48722  gpgprismgrusgra  48974  gpg3nbgrvtx0  48992  gpg3kgrtriexlem1  48999  logbpw2m1  49497