Theorem letrd 10954

Description: Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.)

Hypotheses

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

Assertion

Ref	Expression
letrd	⊢ (𝜑 → 𝐴 ≤ 𝐶)

Proof of Theorem letrd

Step	Hyp	Ref	Expression
1		letrd.4	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
2		letrd.5	. 2 ⊢ (𝜑 → 𝐵 ≤ 𝐶)
3		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		letrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		letr 10891	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
7	3, 4, 5, 6	syl3anc 1373	. 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
8	1, 2, 7	mp2and 699	1 ⊢ (𝜑 → 𝐴 ≤ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2112   class class class wbr 5039  ℝcr 10693   ≤ cle 10833

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501  ax-resscn 10751  ax-pre-lttri 10768  ax-pre-lttrn 10769

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-nel 3037  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-csb 3799  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-er 8369  df-en 8605  df-dom 8606  df-sdom 8607  df-pnf 10834  df-mnf 10835  df-xr 10836  df-ltxr 10837  df-le 10838

This theorem is referenced by:  lesub3d  11415  supmul1  11766  supmul  11769  nn0negleid  12107  eluzuzle  12412  iccsplit  13038  supicc  13054  fzdisj  13104  ssfzunsnext  13122  difelfzle  13190  flwordi  13352  flleceil  13391  uzsup  13401  modltm1p1mod  13461  seqf1olem1  13580  bernneq  13761  bernneq3  13763  discr1  13771  faclbnd  13821  faclbnd4lem1  13824  facubnd  13831  seqcoll  13995  sqrlem7  14777  absle  14844  releabs  14850  absrdbnd  14870  rexuzre  14881  limsupgre  15007  lo1bddrp  15051  rlimclim1  15071  rlimresb  15091  rlimrege0  15105  o1add  15140  o1sub  15142  climsqz  15167  climsqz2  15168  rlimsqzlem  15177  rlimsqz  15178  rlimsqz2  15179  rlimno1  15182  isercoll  15196  caucvgrlem  15201  iseraltlem3  15212  o1fsum  15340  cvgcmp  15343  cvgcmpce  15345  climcnds  15378  expcnv  15391  cvgrat  15410  mertenslem2  15412  fprodle  15521  eftlub  15633  rpnnen2lem12  15749  bitsfzo  15957  isprm5  16227  isprm7  16228  eulerthlem2  16298  pcmpt2  16409  pcfac  16415  prmreclem3  16434  prmreclem4  16435  prmreclem5  16436  4sqlem11  16471  vdwlem1  16497  vdwlem3  16499  setsstruct2  16703  prdsxmetlem  23220  nrmmetd  23426  nm2dif  23477  nlmvscnlem2  23537  nmoco  23589  nmotri  23591  nghmcn  23597  icccmplem2  23674  reconnlem2  23678  elii1  23786  xrhmeo  23797  cnheiborlem  23805  bndth  23809  tcphcphlem1  24086  ipcnlem2  24095  cncmet  24173  trirn  24251  minveclem2  24277  minveclem4  24283  ivthlem2  24303  ovolunlem1a  24347  ovolunlem1  24348  ovolfiniun  24352  ovoliunlem1  24353  ovolicc2lem4  24371  ovolicc2lem5  24372  ovolicopnf  24375  nulmbl2  24387  ioombl1lem4  24412  ioorcl2  24423  uniioombllem3  24436  uniioombllem4  24437  uniioombllem5  24438  volcn  24457  vitalilem2  24460  vitali  24464  mbfi1fseqlem5  24571  mbfi1fseqlem6  24572  itg2splitlem  24600  itg2monolem1  24602  itg2monolem3  24604  itg2mono  24605  itg2cnlem1  24613  itgle  24661  bddmulibl  24690  bddiblnc  24693  ditgsplitlem  24711  dveflem  24830  dvlip  24844  dveq0  24851  dvfsumabs  24874  dvfsumlem1  24877  dvfsumlem2  24878  dvfsumlem3  24879  dvfsumlem4  24880  dvfsum2  24885  fta1glem2  25018  dgradd2  25116  plydiveu  25145  fta1lem  25154  aalioulem2  25180  aalioulem3  25181  aalioulem4  25182  aalioulem5  25183  aaliou3lem8  25192  aaliou3lem9  25197  ulmbdd  25244  ulmcn  25245  mtest  25250  mtestbdd  25251  abelthlem2  25278  abelthlem7  25284  pilem2  25298  tanabsge  25350  cosordlem  25373  tanord  25381  logneg2  25457  abslogle  25460  dvlog2lem  25494  cxple2a  25541  abscxpbnd  25593  atans2  25768  leibpi  25779  o1cxp  25811  cxploglim2  25815  jensenlem2  25824  emcllem6  25837  harmoniclbnd  25845  harmonicubnd  25846  harmonicbnd4  25847  fsumharmonic  25848  lgamgulmlem2  25866  lgamgulmlem3  25867  lgamgulmlem5  25869  lgambdd  25873  ftalem2  25910  basellem3  25919  basellem5  25921  basellem6  25922  dvdsflsumcom  26024  fsumfldivdiaglem  26025  ppiub  26039  chtublem  26046  logfac2  26052  chpub  26055  logfacubnd  26056  logfaclbnd  26057  logfacbnd3  26058  logexprlim  26060  bcmono  26112  bpos1lem  26117  bposlem1  26119  bposlem2  26120  bposlem3  26121  bposlem4  26122  bposlem5  26123  bposlem6  26124  bposlem7  26125  bposlem9  26127  lgsdirprm  26166  lgsquadlem1  26215  2lgslem1c  26228  2sqlem8  26261  chebbnd1lem1  26304  chebbnd1lem3  26306  chtppilimlem1  26308  chpchtlim  26314  vmadivsumb  26318  rplogsumlem1  26319  rplogsumlem2  26320  rpvmasumlem  26322  dchrisumlema  26323  dchrisumlem2  26325  dchrisumlem3  26326  dchrmusum2  26329  dchrvmasumlem2  26333  dchrvmasumlem3  26334  dchrvmasumlema  26335  dchrvmasumiflem1  26336  dchrisum0flblem1  26343  dchrisum0flblem2  26344  dchrisum0fno1  26346  dchrisum0re  26348  dchrisum0lem1b  26350  dchrisum0lem1  26351  dchrisum0lem2a  26352  dchrisum0  26355  rplogsum  26362  mudivsum  26365  mulogsumlem  26366  logdivsum  26368  mulog2sumlem1  26369  mulog2sumlem2  26370  2vmadivsumlem  26375  log2sumbnd  26379  selberglem2  26381  selbergb  26384  selberg2lem  26385  selberg2b  26387  chpdifbndlem1  26388  logdivbnd  26391  selberg3lem1  26392  selberg3lem2  26393  selberg4lem1  26395  pntrmax  26399  pntrsumo1  26400  pntrsumbnd  26401  pntrlog2bndlem1  26412  pntrlog2bndlem2  26413  pntrlog2bndlem3  26414  pntrlog2bndlem5  26416  pntrlog2bndlem6  26418  pntrlog2bnd  26419  pntpbnd1a  26420  pntpbnd1  26421  pntpbnd2  26422  pntibndlem2  26426  pntibndlem3  26427  pntlemg  26433  pntlemr  26437  pntlemj  26438  pntlemf  26440  pntlemk  26441  pntlemo  26442  pntleml  26446  abvcxp  26450  qabvle  26460  padicabv  26465  ostth2lem2  26469  ostth2lem3  26470  ostth3  26473  axlowdimlem16  27002  axcontlem8  27016  axcontlem10  27018  wwlksm1edg  27919  wwlksubclwwlk  28095  smcnlem  28732  nmoub3i  28808  ubthlem3  28907  minvecolem2  28910  minvecolem3  28911  minvecolem4  28915  htthlem  28952  bcs2  29217  pjhthlem1  29426  cnlnadjlem2  30103  cnlnadjlem7  30108  nmopadjlem  30124  nmoptrii  30129  nmopcoadji  30136  leopnmid  30173  cdj1i  30468  nndiffz1  30781  pmtrto1cl  31039  psgnfzto1stlem  31040  fzto1st  31043  psgnfzto1st  31045  cyc3conja  31097  smatrcl  31414  submateqlem1  31425  nexple  31643  esumpcvgval  31712  oddpwdc  31987  eulerpartlems  31993  eulerpartlemgc  31995  eulerpartlemb  32001  dstfrvunirn  32107  orvclteinc  32108  ballotlemsima  32148  ballotlemfrcn0  32162  signstfveq0  32222  fsum2dsub  32253  breprexplemc  32278  breprexp  32279  logdivsqrle  32296  hgt750lemb  32302  hgt750leme  32304  tgoldbachgnn  32305  dnibndlem2  34345  dnibndlem6  34349  dnibndlem9  34352  dnibndlem10  34353  dnibndlem11  34354  dnibndlem12  34355  knoppcnlem4  34362  unblimceq0lem  34372  unblimceq0  34373  unbdqndv2lem2  34376  knoppndvlem11  34388  knoppndvlem14  34391  knoppndvlem15  34392  knoppndvlem18  34395  knoppndvlem21  34398  poimirlem6  35469  poimirlem7  35470  poimirlem13  35476  poimirlem15  35478  poimirlem29  35492  mblfinlem2  35501  mblfinlem3  35502  mblfinlem4  35503  ismblfin  35504  itg2addnc  35517  iblmulc2nc  35528  ftc1anclem7  35542  ftc1anclem8  35543  filbcmb  35584  geomcau  35603  prdsbnd  35637  cntotbnd  35640  bfplem2  35667  rrntotbnd  35680  iccbnd  35684  lcmineqlem20  39739  lcmineqlem21  39740  lcmineqlem22  39741  3lexlogpow5ineq2  39746  3lexlogpow5ineq5  39751  aks4d1p1p2  39760  aks4d1p1p4  39761  aks4d1p1p7  39764  aks4d1p1p5  39765  aks4d1p1  39766  2np3bcnp1  39769  sticksstones6  39776  sticksstones7  39777  sticksstones10  39780  sticksstones12a  39782  sticksstones12  39783  metakunt1  39788  metakunt12  39799  metakunt28  39815  lzunuz  40234  irrapxlem3  40290  irrapxlem4  40291  irrapxlem5  40292  pellexlem2  40296  pell1qrge1  40336  monotoddzzfi  40408  jm2.17a  40426  rmygeid  40430  fzmaxdif  40447  jm2.27c  40473  jm3.1lem1  40483  expdiophlem1  40487  imo72b2lem0  41394  int-ineqtransd  41424  dvgrat  41544  monoords  42450  absnpncan2d  42455  absnpncan3d  42460  ssfiunibd  42462  leadd12dd  42469  rexabslelem  42572  uzublem  42584  sqrlearg  42707  fmul01  42739  fmul01lt1lem1  42743  fmul01lt1lem2  42744  climsuselem1  42766  climsuse  42767  limsupresico  42859  limsupubuzlem  42871  limsupmnfuzlem  42885  limsupre3uzlem  42894  liminfresico  42930  limsup10exlem  42931  cnrefiisplem  42988  dvdivbd  43082  dvbdfbdioolem2  43088  ioodvbdlimc1lem1  43090  ioodvbdlimc1lem2  43091  ioodvbdlimc2lem  43093  dvnmul  43102  dvnprodlem1  43105  dvnprodlem2  43106  iblspltprt  43132  itgspltprt  43138  stoweidlem1  43160  stoweidlem3  43162  stoweidlem5  43164  stoweidlem11  43170  stoweidlem17  43176  stoweidlem20  43179  stoweidlem26  43185  stoweidlem34  43193  wallispilem4  43227  stirlinglem11  43243  stirlinglem12  43244  stirlinglem13  43245  fourierdlem12  43278  fourierdlem15  43281  fourierdlem20  43286  fourierdlem30  43296  fourierdlem39  43305  fourierdlem42  43308  fourierdlem47  43312  fourierdlem50  43315  fourierdlem64  43329  fourierdlem65  43330  fourierdlem68  43333  fourierdlem73  43338  fourierdlem77  43342  fourierdlem79  43344  fourierdlem87  43352  elaa2lem  43392  etransclem23  43416  ioorrnopnlem  43463  salgencntex  43500  sge0le  43563  sge0isum  43583  sge0xaddlem1  43589  hoicvr  43704  hsphoidmvle2  43741  hoidmv1lelem1  43747  hoidmv1lelem2  43748  hoidmv1lelem3  43749  hoidmvlelem1  43751  hoidmvlelem2  43752  hoidmvlelem4  43754  hspmbllem1  43782  hspmbllem2  43783  smfmullem1  43940  smfmullem2  43941  smfmullem3  43942  smfsuplem1  43959  lighneallem4a  44676  fllog2  45530  itcovalt2lem2lem1  45635