Theorem letrd 10644

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2081   class class class wbr 4962  ℝcr 10382   ≤ cle 10522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319  ax-resscn 10440  ax-pre-lttri 10457  ax-pre-lttrn 10458

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ne 2985  df-nel 3091  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-res 5455  df-ima 5456  df-iota 6189  df-fun 6227  df-fn 6228  df-f 6229  df-f1 6230  df-fo 6231  df-f1o 6232  df-fv 6233  df-er 8139  df-en 8358  df-dom 8359  df-sdom 8360  df-pnf 10523  df-mnf 10524  df-xr 10525  df-ltxr 10526  df-le 10527

This theorem is referenced by:  lesub3d  11106  supmul1  11458  supmul  11461  nn0negleid  11797  eluzuzle  12102  iccsplit  12721  supicc  12736  fzdisj  12784  ssfzunsnext  12802  difelfzle  12870  flwordi  13032  flleceil  13071  uzsup  13081  modltm1p1mod  13141  seqf1olem1  13259  bernneq  13440  bernneq3  13442  discr1  13450  faclbnd  13500  faclbnd4lem1  13503  facubnd  13510  seqcoll  13670  sqrlem7  14442  absle  14509  releabs  14515  absrdbnd  14535  rexuzre  14546  limsupgre  14672  lo1bddrp  14716  rlimclim1  14736  rlimresb  14756  rlimrege0  14770  o1add  14804  o1sub  14806  climsqz  14831  climsqz2  14832  rlimsqzlem  14839  rlimsqz  14840  rlimsqz2  14841  rlimno1  14844  isercoll  14858  caucvgrlem  14863  iseraltlem3  14874  o1fsum  15001  cvgcmp  15004  cvgcmpce  15006  climcnds  15039  expcnv  15052  cvgrat  15072  mertenslem2  15074  fprodle  15183  eftlub  15295  rpnnen2lem12  15411  bitsfzo  15617  isprm5  15880  isprm7  15881  eulerthlem2  15948  pcmpt2  16058  pcfac  16064  prmreclem3  16083  prmreclem4  16084  prmreclem5  16085  4sqlem11  16120  vdwlem1  16146  vdwlem3  16148  setsstruct2  16350  prdsxmetlem  22661  nrmmetd  22867  nm2dif  22917  nlmvscnlem2  22977  nmoco  23029  nmotri  23031  nghmcn  23037  icccmplem2  23114  reconnlem2  23118  elii1  23222  xrhmeo  23233  cnheiborlem  23241  bndth  23245  tcphcphlem1  23521  ipcnlem2  23530  cncmet  23608  trirn  23686  minveclem2  23712  minveclem4  23718  ivthlem2  23736  ovolunlem1a  23780  ovolunlem1  23781  ovolfiniun  23785  ovoliunlem1  23786  ovolicc2lem4  23804  ovolicc2lem5  23805  ovolicopnf  23808  nulmbl2  23820  ioombl1lem4  23845  ioorcl2  23856  uniioombllem3  23869  uniioombllem4  23870  uniioombllem5  23871  volcn  23890  vitalilem2  23893  vitali  23897  mbfi1fseqlem5  24003  mbfi1fseqlem6  24004  itg2splitlem  24032  itg2monolem1  24034  itg2monolem3  24036  itg2mono  24037  itg2cnlem1  24045  itgle  24093  bddmulibl  24122  ditgsplitlem  24141  dveflem  24259  dvlip  24273  dveq0  24280  dvfsumabs  24303  dvfsumlem1  24306  dvfsumlem2  24307  dvfsumlem3  24308  dvfsumlem4  24309  dvfsum2  24314  fta1glem2  24443  dgradd2  24541  plydiveu  24570  fta1lem  24579  aalioulem2  24605  aalioulem3  24606  aalioulem4  24607  aalioulem5  24608  aaliou3lem8  24617  aaliou3lem9  24622  ulmbdd  24669  ulmcn  24670  mtest  24675  mtestbdd  24676  abelthlem2  24703  abelthlem7  24709  pilem2  24723  tanabsge  24775  cosordlem  24796  tanord  24803  logneg2  24879  abslogle  24882  dvlog2lem  24916  cxple2a  24963  abscxpbnd  25015  atans2  25190  leibpi  25202  o1cxp  25234  cxploglim2  25238  jensenlem2  25247  emcllem6  25260  harmoniclbnd  25268  harmonicubnd  25269  harmonicbnd4  25270  fsumharmonic  25271  lgamgulmlem2  25289  lgamgulmlem3  25290  lgamgulmlem5  25292  lgambdd  25296  ftalem2  25333  basellem3  25342  basellem5  25344  basellem6  25345  dvdsflsumcom  25447  fsumfldivdiaglem  25448  ppiub  25462  chtublem  25469  logfac2  25475  chpub  25478  logfacubnd  25479  logfaclbnd  25480  logfacbnd3  25481  logexprlim  25483  bcmono  25535  bpos1lem  25540  bposlem1  25542  bposlem2  25543  bposlem3  25544  bposlem4  25545  bposlem5  25546  bposlem6  25547  bposlem7  25548  bposlem9  25550  lgsdirprm  25589  lgsquadlem1  25638  2lgslem1c  25651  2sqlem8  25684  chebbnd1lem1  25727  chebbnd1lem3  25729  chtppilimlem1  25731  chpchtlim  25737  vmadivsumb  25741  rplogsumlem1  25742  rplogsumlem2  25743  rpvmasumlem  25745  dchrisumlema  25746  dchrisumlem2  25748  dchrisumlem3  25749  dchrmusum2  25752  dchrvmasumlem2  25756  dchrvmasumlem3  25757  dchrvmasumlema  25758  dchrvmasumiflem1  25759  dchrisum0flblem1  25766  dchrisum0flblem2  25767  dchrisum0fno1  25769  dchrisum0re  25771  dchrisum0lem1b  25773  dchrisum0lem1  25774  dchrisum0lem2a  25775  dchrisum0  25778  rplogsum  25785  mudivsum  25788  mulogsumlem  25789  logdivsum  25791  mulog2sumlem1  25792  mulog2sumlem2  25793  2vmadivsumlem  25798  log2sumbnd  25802  selberglem2  25804  selbergb  25807  selberg2lem  25808  selberg2b  25810  chpdifbndlem1  25811  logdivbnd  25814  selberg3lem1  25815  selberg3lem2  25816  selberg4lem1  25818  pntrmax  25822  pntrsumo1  25823  pntrsumbnd  25824  pntrlog2bndlem1  25835  pntrlog2bndlem2  25836  pntrlog2bndlem3  25837  pntrlog2bndlem5  25839  pntrlog2bndlem6  25841  pntrlog2bnd  25842  pntpbnd1a  25843  pntpbnd1  25844  pntpbnd2  25845  pntibndlem2  25849  pntibndlem3  25850  pntlemg  25856  pntlemr  25860  pntlemj  25861  pntlemf  25863  pntlemk  25864  pntlemo  25865  pntleml  25869  abvcxp  25873  qabvle  25883  padicabv  25888  ostth2lem2  25892  ostth2lem3  25893  ostth3  25896  axlowdimlem16  26426  axcontlem8  26440  axcontlem10  26442  wwlksm1edg  27346  wwlksubclwwlk  27524  smcnlem  28165  nmoub3i  28241  ubthlem3  28340  minvecolem2  28343  minvecolem3  28344  minvecolem4  28348  htthlem  28385  bcs2  28650  pjhthlem1  28859  cnlnadjlem2  29536  cnlnadjlem7  29541  nmopadjlem  29557  nmoptrii  29562  nmopcoadji  29569  leopnmid  29606  cdj1i  29901  nndiffz1  30197  cyc3conja  30437  pmtrto1cl  30663  psgnfzto1stlem  30664  fzto1st  30667  psgnfzto1st  30669  smatrcl  30676  submateqlem1  30687  nexple  30885  esumpcvgval  30954  oddpwdc  31229  eulerpartlems  31235  eulerpartlemgc  31237  eulerpartlemb  31243  dstfrvunirn  31349  orvclteinc  31350  ballotlemsima  31390  ballotlemfrcn0  31404  signstfveq0  31464  fsum2dsub  31495  breprexplemc  31520  breprexp  31521  logdivsqrle  31538  hgt750lemb  31544  hgt750leme  31546  tgoldbachgnn  31547  dnibndlem2  33427  dnibndlem6  33431  dnibndlem9  33434  dnibndlem10  33435  dnibndlem11  33436  dnibndlem12  33437  knoppcnlem4  33444  unblimceq0lem  33454  unblimceq0  33455  unbdqndv2lem2  33458  knoppndvlem11  33470  knoppndvlem14  33473  knoppndvlem15  33474  knoppndvlem18  33477  knoppndvlem21  33480  poimirlem6  34429  poimirlem7  34430  poimirlem13  34436  poimirlem15  34438  poimirlem29  34452  mblfinlem2  34461  mblfinlem3  34462  mblfinlem4  34463  ismblfin  34464  itg2addnc  34477  iblmulc2nc  34488  bddiblnc  34493  ftc1anclem7  34504  ftc1anclem8  34505  filbcmb  34547  geomcau  34566  prdsbnd  34603  cntotbnd  34606  bfplem2  34633  rrntotbnd  34646  iccbnd  34650  lzunuz  38850  irrapxlem3  38906  irrapxlem4  38907  irrapxlem5  38908  pellexlem2  38912  pell1qrge1  38952  monotoddzzfi  39024  jm2.17a  39042  rmygeid  39046  fzmaxdif  39063  jm2.27c  39089  jm3.1lem1  39099  expdiophlem1  39103  imo72b2lem0  40001  int-ineqtransd  40033  dvgrat  40182  monoords  41105  absnpncan2d  41110  absnpncan3d  41115  ssfiunibd  41117  leadd12dd  41125  rexabslelem  41234  uzublem  41246  sqrlearg  41371  fmul01  41403  fmul01lt1lem1  41407  fmul01lt1lem2  41408  climsuselem1  41430  climsuse  41431  limsupresico  41523  limsupubuzlem  41535  limsupmnfuzlem  41549  limsupre3uzlem  41558  liminfresico  41594  limsup10exlem  41595  cnrefiisplem  41652  dvdivbd  41749  dvbdfbdioolem2  41755  ioodvbdlimc1lem1  41757  ioodvbdlimc1lem2  41758  ioodvbdlimc2lem  41760  dvnmul  41769  dvnprodlem1  41772  dvnprodlem2  41773  iblspltprt  41799  itgspltprt  41805  stoweidlem1  41828  stoweidlem3  41830  stoweidlem5  41832  stoweidlem11  41838  stoweidlem17  41844  stoweidlem20  41847  stoweidlem26  41853  stoweidlem34  41861  wallispilem4  41895  stirlinglem11  41911  stirlinglem12  41912  stirlinglem13  41913  fourierdlem12  41946  fourierdlem15  41949  fourierdlem20  41954  fourierdlem30  41964  fourierdlem39  41973  fourierdlem42  41976  fourierdlem47  41980  fourierdlem50  41983  fourierdlem64  41997  fourierdlem65  41998  fourierdlem68  42001  fourierdlem73  42006  fourierdlem77  42010  fourierdlem79  42012  fourierdlem87  42020  elaa2lem  42060  etransclem23  42084  ioorrnopnlem  42131  salgencntex  42168  sge0le  42231  sge0isum  42251  sge0xaddlem1  42257  hoicvr  42372  hsphoidmvle2  42409  hoidmv1lelem1  42415  hoidmv1lelem2  42416  hoidmv1lelem3  42417  hoidmvlelem1  42419  hoidmvlelem2  42420  hoidmvlelem4  42422  hspmbllem1  42450  hspmbllem2  42451  smfmullem1  42608  smfmullem2  42609  smfmullem3  42610  smfsuplem1  42627  lighneallem4a  43255  fllog2  44109