Theorem letrd 11368

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   class class class wbr 5148  ℝcr 11106   ≤ cle 11246

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-resscn 11164  ax-pre-lttri 11181  ax-pre-lttrn 11182

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251

This theorem is referenced by:  lesub3d  11829  supmul1  12180  supmul  12183  nn0negleid  12521  eluzuzle  12828  iccsplit  13459  supicc  13475  fzdisj  13525  ssfzunsnext  13543  difelfzle  13611  flwordi  13774  flleceil  13815  uzsup  13825  modltm1p1mod  13885  seqf1olem1  14004  zzlesq  14167  bernneq  14189  bernneq3  14191  discr1  14199  faclbnd  14247  faclbnd4lem1  14250  facubnd  14257  seqcoll  14422  01sqrexlem7  15192  absle  15259  releabs  15265  absrdbnd  15285  rexuzre  15296  limsupgre  15422  lo1bddrp  15466  rlimclim1  15486  rlimresb  15506  rlimrege0  15520  o1add  15555  o1sub  15557  climsqz  15582  climsqz2  15583  rlimsqzlem  15592  rlimsqz  15593  rlimsqz2  15594  rlimno1  15597  isercoll  15611  caucvgrlem  15616  iseraltlem3  15627  o1fsum  15756  cvgcmp  15759  cvgcmpce  15761  climcnds  15794  expcnv  15807  cvgrat  15826  mertenslem2  15828  fprodle  15937  eftlub  16049  rpnnen2lem12  16165  bitsfzo  16373  isprm5  16641  isprm7  16642  eulerthlem2  16712  pcmpt2  16823  pcfac  16829  prmreclem3  16848  prmreclem4  16849  prmreclem5  16850  4sqlem11  16885  vdwlem1  16911  vdwlem3  16913  setsstruct2  17104  prdsxmetlem  23866  nrmmetd  24075  nm2dif  24126  nlmvscnlem2  24194  nmoco  24246  nmotri  24248  nghmcn  24254  icccmplem2  24331  reconnlem2  24335  elii1  24443  xrhmeo  24454  cnheiborlem  24462  bndth  24466  tcphcphlem1  24744  ipcnlem2  24753  cncmet  24831  trirn  24909  minveclem2  24935  minveclem4  24941  ivthlem2  24961  ovolunlem1a  25005  ovolunlem1  25006  ovolfiniun  25010  ovoliunlem1  25011  ovolicc2lem4  25029  ovolicc2lem5  25030  ovolicopnf  25033  nulmbl2  25045  ioombl1lem4  25070  ioorcl2  25081  uniioombllem3  25094  uniioombllem4  25095  uniioombllem5  25096  volcn  25115  vitalilem2  25118  vitali  25122  mbfi1fseqlem5  25229  mbfi1fseqlem6  25230  itg2splitlem  25258  itg2monolem1  25260  itg2monolem3  25262  itg2mono  25263  itg2cnlem1  25271  itgle  25319  bddmulibl  25348  bddiblnc  25351  ditgsplitlem  25369  dveflem  25488  dvlip  25502  dveq0  25509  dvfsumabs  25532  dvfsumlem1  25535  dvfsumlem2  25536  dvfsumlem3  25537  dvfsumlem4  25538  dvfsum2  25543  fta1glem2  25676  dgradd2  25774  plydiveu  25803  fta1lem  25812  aalioulem2  25838  aalioulem3  25839  aalioulem4  25840  aalioulem5  25841  aaliou3lem8  25850  aaliou3lem9  25855  ulmbdd  25902  ulmcn  25903  mtest  25908  mtestbdd  25909  abelthlem2  25936  abelthlem7  25942  pilem2  25956  tanabsge  26008  cosordlem  26031  tanord  26039  logneg2  26115  abslogle  26118  dvlog2lem  26152  cxple2a  26199  abscxpbnd  26251  atans2  26426  leibpi  26437  o1cxp  26469  cxploglim2  26473  jensenlem2  26482  emcllem6  26495  harmoniclbnd  26503  harmonicubnd  26504  harmonicbnd4  26505  fsumharmonic  26506  lgamgulmlem2  26524  lgamgulmlem3  26525  lgamgulmlem5  26527  lgambdd  26531  ftalem2  26568  basellem3  26577  basellem5  26579  basellem6  26580  dvdsflsumcom  26682  fsumfldivdiaglem  26683  ppiub  26697  chtublem  26704  logfac2  26710  chpub  26713  logfacubnd  26714  logfaclbnd  26715  logfacbnd3  26716  logexprlim  26718  bcmono  26770  bpos1lem  26775  bposlem1  26777  bposlem2  26778  bposlem3  26779  bposlem4  26780  bposlem5  26781  bposlem6  26782  bposlem7  26783  bposlem9  26785  lgsdirprm  26824  lgsquadlem1  26873  2lgslem1c  26886  2sqlem8  26919  chebbnd1lem1  26962  chebbnd1lem3  26964  chtppilimlem1  26966  chpchtlim  26972  vmadivsumb  26976  rplogsumlem1  26977  rplogsumlem2  26978  rpvmasumlem  26980  dchrisumlema  26981  dchrisumlem2  26983  dchrisumlem3  26984  dchrmusum2  26987  dchrvmasumlem2  26991  dchrvmasumlem3  26992  dchrvmasumlema  26993  dchrvmasumiflem1  26994  dchrisum0flblem1  27001  dchrisum0flblem2  27002  dchrisum0fno1  27004  dchrisum0re  27006  dchrisum0lem1b  27008  dchrisum0lem1  27009  dchrisum0lem2a  27010  dchrisum0  27013  rplogsum  27020  mudivsum  27023  mulogsumlem  27024  logdivsum  27026  mulog2sumlem1  27027  mulog2sumlem2  27028  2vmadivsumlem  27033  log2sumbnd  27037  selberglem2  27039  selbergb  27042  selberg2lem  27043  selberg2b  27045  chpdifbndlem1  27046  logdivbnd  27049  selberg3lem1  27050  selberg3lem2  27051  selberg4lem1  27053  pntrmax  27057  pntrsumo1  27058  pntrsumbnd  27059  pntrlog2bndlem1  27070  pntrlog2bndlem2  27071  pntrlog2bndlem3  27072  pntrlog2bndlem5  27074  pntrlog2bndlem6  27076  pntrlog2bnd  27077  pntpbnd1a  27078  pntpbnd1  27079  pntpbnd2  27080  pntibndlem2  27084  pntibndlem3  27085  pntlemg  27091  pntlemr  27095  pntlemj  27096  pntlemf  27098  pntlemk  27099  pntlemo  27100  pntleml  27104  abvcxp  27108  qabvle  27118  padicabv  27123  ostth2lem2  27127  ostth2lem3  27128  ostth3  27131  axlowdimlem16  28205  axcontlem8  28219  axcontlem10  28221  wwlksm1edg  29125  wwlksubclwwlk  29301  smcnlem  29938  nmoub3i  30014  ubthlem3  30113  minvecolem2  30116  minvecolem3  30117  minvecolem4  30121  htthlem  30158  bcs2  30423  pjhthlem1  30632  cnlnadjlem2  31309  cnlnadjlem7  31314  nmopadjlem  31330  nmoptrii  31335  nmopcoadji  31342  leopnmid  31379  cdj1i  31674  nndiffz1  31985  pmtrto1cl  32246  psgnfzto1stlem  32247  fzto1st  32250  psgnfzto1st  32252  cyc3conja  32304  smatrcl  32765  submateqlem1  32776  nexple  32996  esumpcvgval  33065  oddpwdc  33342  eulerpartlems  33348  eulerpartlemgc  33350  eulerpartlemb  33356  dstfrvunirn  33462  orvclteinc  33463  ballotlemsima  33503  ballotlemfrcn0  33517  signstfveq0  33577  fsum2dsub  33608  breprexplemc  33633  breprexp  33634  logdivsqrle  33651  hgt750lemb  33657  hgt750leme  33659  tgoldbachgnn  33660  gg-dvfsumlem2  35172  dnibndlem2  35344  dnibndlem6  35348  dnibndlem9  35351  dnibndlem10  35352  dnibndlem11  35353  dnibndlem12  35354  knoppcnlem4  35361  unblimceq0lem  35371  unblimceq0  35372  unbdqndv2lem2  35375  knoppndvlem11  35387  knoppndvlem14  35390  knoppndvlem15  35391  knoppndvlem18  35394  knoppndvlem21  35397  poimirlem6  36483  poimirlem7  36484  poimirlem13  36490  poimirlem15  36492  poimirlem29  36506  mblfinlem2  36515  mblfinlem3  36516  mblfinlem4  36517  ismblfin  36518  itg2addnc  36531  iblmulc2nc  36542  ftc1anclem7  36556  ftc1anclem8  36557  filbcmb  36597  geomcau  36616  prdsbnd  36650  cntotbnd  36653  bfplem2  36680  rrntotbnd  36693  iccbnd  36697  lcmineqlem20  40902  lcmineqlem21  40903  lcmineqlem22  40904  3lexlogpow5ineq2  40909  3lexlogpow5ineq5  40914  aks4d1p1p2  40924  aks4d1p1p4  40925  aks4d1p1p7  40928  aks4d1p1p5  40929  aks4d1p1  40930  aks4d1p2  40931  aks4d1p3  40932  aks4d1p5  40934  aks4d1p6  40935  aks4d1p7d1  40936  aks4d1p7  40937  aks4d1p8  40941  2np3bcnp1  40949  sticksstones6  40956  sticksstones7  40957  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  sticksstones22  40973  metakunt1  40974  metakunt12  40985  metakunt28  41001  lzunuz  41492  irrapxlem3  41548  irrapxlem4  41549  irrapxlem5  41550  pellexlem2  41554  pell1qrge1  41594  monotoddzzfi  41667  jm2.17a  41685  rmygeid  41689  fzmaxdif  41706  jm2.27c  41732  jm3.1lem1  41742  expdiophlem1  41746  fzunt  42192  fzuntd  42193  fzunt1d  42194  fzuntgd  42195  imo72b2lem0  42903  int-ineqtransd  42932  dvgrat  43057  monoords  43994  absnpncan2d  43999  absnpncan3d  44004  ssfiunibd  44006  leadd12dd  44013  rexabslelem  44115  uzublem  44127  sqrlearg  44253  fmul01  44283  fmul01lt1lem1  44287  fmul01lt1lem2  44288  climsuselem1  44310  climsuse  44311  limsupresico  44403  limsupubuzlem  44415  limsupmnfuzlem  44429  limsupre3uzlem  44438  liminfresico  44474  limsup10exlem  44475  cnrefiisplem  44532  dvdivbd  44626  dvbdfbdioolem2  44632  ioodvbdlimc1lem1  44634  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvnmul  44646  dvnprodlem1  44649  dvnprodlem2  44650  iblspltprt  44676  itgspltprt  44682  stoweidlem1  44704  stoweidlem3  44706  stoweidlem5  44708  stoweidlem11  44714  stoweidlem17  44720  stoweidlem20  44723  stoweidlem26  44729  stoweidlem34  44737  wallispilem4  44771  stirlinglem11  44787  stirlinglem12  44788  stirlinglem13  44789  fourierdlem12  44822  fourierdlem15  44825  fourierdlem20  44830  fourierdlem30  44840  fourierdlem39  44849  fourierdlem42  44852  fourierdlem47  44856  fourierdlem50  44859  fourierdlem64  44873  fourierdlem65  44874  fourierdlem68  44877  fourierdlem73  44882  fourierdlem77  44886  fourierdlem79  44888  fourierdlem87  44896  elaa2lem  44936  etransclem23  44960  ioorrnopnlem  45007  salgencntex  45046  sge0le  45110  sge0isum  45130  sge0xaddlem1  45136  hoicvr  45251  hsphoidmvle2  45288  hoidmv1lelem1  45294  hoidmv1lelem2  45295  hoidmv1lelem3  45296  hoidmvlelem1  45298  hoidmvlelem2  45299  hoidmvlelem4  45301  hspmbllem1  45329  hspmbllem2  45330  smfmullem1  45494  smfmullem2  45495  smfmullem3  45496  smfsuplem1  45514  natglobalincr  45578  lighneallem4a  46263  fllog2  47208  itcovalt2lem2lem1  47313