Theorem letrd 11288

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 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 5096  ℝcr 11023   ≤ cle 11165

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 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-pre-lttri 11098  ax-pre-lttrn 11099

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 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170

This theorem is referenced by:  lesub3d  11753  le2addd  11754  supmul1  12109  supmul  12112  nn0negleid  12451  eluzuzle  12758  iccsplit  13399  supicc  13415  fzdisj  13465  ssfzunsnext  13483  difelfzle  13555  flwordi  13730  flleceil  13771  uzsup  13781  modltm1p1mod  13844  seqf1olem1  13962  zzlesq  14127  bernneq  14150  bernneq3  14152  discr1  14160  faclbnd  14211  faclbnd4lem1  14214  facubnd  14221  seqcoll  14385  01sqrexlem7  15169  absle  15237  releabs  15243  absrdbnd  15263  rexuzre  15274  limsupgre  15402  lo1bddrp  15446  rlimclim1  15466  rlimresb  15486  rlimrege0  15500  o1add  15535  o1sub  15537  climsqz  15562  climsqz2  15563  rlimsqzlem  15570  rlimsqz  15571  rlimsqz2  15572  rlimno1  15575  isercoll  15589  caucvgrlem  15594  iseraltlem3  15605  o1fsum  15734  cvgcmp  15737  cvgcmpce  15739  climcnds  15772  expcnv  15785  cvgrat  15804  mertenslem2  15806  fprodle  15917  eftlub  16032  rpnnen2lem12  16148  bitsfzo  16360  isprm5  16632  isprm7  16633  eulerthlem2  16707  pcmpt2  16819  pcfac  16825  prmreclem3  16844  prmreclem4  16845  prmreclem5  16846  4sqlem11  16881  vdwlem1  16907  vdwlem3  16909  setsstruct2  17099  prdsxmetlem  24310  nrmmetd  24516  nm2dif  24567  nlmvscnlem2  24627  nmoco  24679  nmotri  24681  nghmcn  24687  icccmplem2  24766  reconnlem2  24770  elii1  24885  xrhmeo  24898  cnheiborlem  24907  bndth  24911  tcphcphlem1  25189  ipcnlem2  25198  cncmet  25276  trirn  25354  minveclem2  25380  minveclem4  25386  ivthlem2  25407  ovolunlem1a  25451  ovolunlem1  25452  ovolfiniun  25456  ovoliunlem1  25457  ovolicc2lem4  25475  ovolicc2lem5  25476  ovolicopnf  25479  nulmbl2  25491  ioombl1lem4  25516  ioorcl2  25527  uniioombllem3  25540  uniioombllem4  25541  uniioombllem5  25542  volcn  25561  vitalilem2  25564  vitali  25568  mbfi1fseqlem5  25674  mbfi1fseqlem6  25675  itg2splitlem  25703  itg2monolem1  25705  itg2monolem3  25707  itg2mono  25708  itg2cnlem1  25716  itgle  25765  bddmulibl  25794  bddiblnc  25797  ditgsplitlem  25815  dveflem  25937  dvlip  25952  dveq0  25959  dvfsumabs  25983  dvfsumlem1  25986  dvfsumlem2  25987  dvfsumlem2OLD  25988  dvfsumlem3  25989  dvfsumlem4  25990  dvfsum2  25995  fta1glem2  26128  dgradd2  26228  plydiveu  26260  fta1lem  26269  aalioulem2  26295  aalioulem3  26296  aalioulem4  26297  aalioulem5  26298  aaliou3lem8  26307  aaliou3lem9  26312  ulmbdd  26361  ulmcn  26362  mtest  26367  mtestbdd  26368  abelthlem2  26396  abelthlem7  26402  pilem2  26416  tanabsge  26469  cosordlem  26493  tanord  26501  logneg2  26578  abslogle  26581  dvlog2lem  26615  cxple2a  26662  abscxpbnd  26717  atans2  26895  leibpi  26906  o1cxp  26939  cxploglim2  26943  jensenlem2  26952  emcllem6  26965  harmoniclbnd  26973  harmonicubnd  26974  harmonicbnd4  26975  fsumharmonic  26976  lgamgulmlem2  26994  lgamgulmlem3  26995  lgamgulmlem5  26997  lgambdd  27001  ftalem2  27038  basellem3  27047  basellem5  27049  basellem6  27050  dvdsflsumcom  27152  fsumfldivdiaglem  27153  ppiub  27169  chtublem  27176  logfac2  27182  chpub  27185  logfacubnd  27186  logfaclbnd  27187  logfacbnd3  27188  logexprlim  27190  bcmono  27242  bpos1lem  27247  bposlem1  27249  bposlem2  27250  bposlem3  27251  bposlem4  27252  bposlem5  27253  bposlem6  27254  bposlem7  27255  bposlem9  27257  lgsdirprm  27296  lgsquadlem1  27345  2lgslem1c  27358  2sqlem8  27391  chebbnd1lem1  27434  chebbnd1lem3  27436  chtppilimlem1  27438  chpchtlim  27444  vmadivsumb  27448  rplogsumlem1  27449  rplogsumlem2  27450  rpvmasumlem  27452  dchrisumlema  27453  dchrisumlem2  27455  dchrisumlem3  27456  dchrmusum2  27459  dchrvmasumlem2  27463  dchrvmasumlem3  27464  dchrvmasumlema  27465  dchrvmasumiflem1  27466  dchrisum0flblem1  27473  dchrisum0flblem2  27474  dchrisum0fno1  27476  dchrisum0re  27478  dchrisum0lem1b  27480  dchrisum0lem1  27481  dchrisum0lem2a  27482  dchrisum0  27485  rplogsum  27492  mudivsum  27495  mulogsumlem  27496  logdivsum  27498  mulog2sumlem1  27499  mulog2sumlem2  27500  2vmadivsumlem  27505  log2sumbnd  27509  selberglem2  27511  selbergb  27514  selberg2lem  27515  selberg2b  27517  chpdifbndlem1  27518  logdivbnd  27521  selberg3lem1  27522  selberg3lem2  27523  selberg4lem1  27525  pntrmax  27529  pntrsumo1  27530  pntrsumbnd  27531  pntrlog2bndlem1  27542  pntrlog2bndlem2  27543  pntrlog2bndlem3  27544  pntrlog2bndlem5  27546  pntrlog2bndlem6  27548  pntrlog2bnd  27549  pntpbnd1a  27550  pntpbnd1  27551  pntpbnd2  27552  pntibndlem2  27556  pntibndlem3  27557  pntlemg  27563  pntlemr  27567  pntlemj  27568  pntlemf  27570  pntlemk  27571  pntlemo  27572  pntleml  27576  abvcxp  27580  qabvle  27590  padicabv  27595  ostth2lem2  27599  ostth2lem3  27600  ostth3  27603  axlowdimlem16  28979  axcontlem8  28993  axcontlem10  28995  wwlksm1edg  29903  wwlksubclwwlk  30082  smcnlem  30721  nmoub3i  30797  ubthlem3  30896  minvecolem2  30899  minvecolem3  30900  minvecolem4  30904  htthlem  30941  bcs2  31206  pjhthlem1  31415  cnlnadjlem2  32092  cnlnadjlem7  32097  nmopadjlem  32113  nmoptrii  32118  nmopcoadji  32125  leopnmid  32162  cdj1i  32457  nndiffz1  32815  nexple  32874  oexpled  32877  pmtrto1cl  33130  psgnfzto1stlem  33131  fzto1st  33134  psgnfzto1st  33136  cyc3conja  33188  constrresqrtcl  33883  cos9thpiminplylem1  33888  smatrcl  33902  submateqlem1  33913  esumpcvgval  34184  oddpwdc  34460  eulerpartlems  34466  eulerpartlemgc  34468  eulerpartlemb  34474  dstfrvunirn  34581  orvclteinc  34582  ballotlemsima  34622  ballotlemfrcn0  34636  signstfveq0  34683  fsum2dsub  34713  breprexplemc  34738  breprexp  34739  logdivsqrle  34756  hgt750lemb  34762  hgt750leme  34764  tgoldbachgnn  34765  dnibndlem2  36622  dnibndlem6  36626  dnibndlem9  36629  dnibndlem10  36630  dnibndlem11  36631  dnibndlem12  36632  knoppcnlem4  36639  unblimceq0lem  36649  unblimceq0  36650  unbdqndv2lem2  36653  knoppndvlem11  36665  knoppndvlem14  36668  knoppndvlem15  36669  knoppndvlem18  36672  knoppndvlem21  36675  poimirlem6  37766  poimirlem7  37767  poimirlem13  37773  poimirlem15  37775  poimirlem29  37789  mblfinlem2  37798  mblfinlem3  37799  mblfinlem4  37800  ismblfin  37801  itg2addnc  37814  iblmulc2nc  37825  ftc1anclem7  37839  ftc1anclem8  37840  filbcmb  37880  geomcau  37899  prdsbnd  37933  cntotbnd  37936  bfplem2  37963  rrntotbnd  37976  iccbnd  37980  lcmineqlem20  42241  lcmineqlem21  42242  lcmineqlem22  42243  3lexlogpow5ineq2  42248  3lexlogpow5ineq5  42253  aks4d1p1p2  42263  aks4d1p1p4  42264  aks4d1p1p7  42267  aks4d1p1p5  42268  aks4d1p1  42269  aks4d1p2  42270  aks4d1p3  42271  aks4d1p5  42273  aks4d1p6  42274  aks4d1p7d1  42275  aks4d1p7  42276  aks4d1p8  42280  posbezout  42293  aks6d1c1  42309  aks6d1c2lem4  42320  2np3bcnp1  42337  sticksstones6  42344  sticksstones7  42345  sticksstones10  42348  sticksstones12a  42350  sticksstones12  42351  sticksstones22  42361  bcled  42371  bcle2d  42372  aks6d1c7lem1  42373  aks6d1c7lem2  42374  unitscyglem4  42391  lzunuz  42952  irrapxlem3  43008  irrapxlem4  43009  irrapxlem5  43010  pellexlem2  43014  pell1qrge1  43054  monotoddzzfi  43126  jm2.17a  43144  rmygeid  43148  fzmaxdif  43165  jm2.27c  43191  jm3.1lem1  43201  expdiophlem1  43205  fzunt  43638  fzuntd  43639  fzunt1d  43640  fzuntgd  43641  imo72b2lem0  44348  int-ineqtransd  44377  dvgrat  44495  monoords  45487  absnpncan2d  45492  absnpncan3d  45497  ssfiunibd  45499  rexabslelem  45604  uzublem  45616  sqrlearg  45741  fmul01  45768  fmul01lt1lem1  45772  fmul01lt1lem2  45773  climsuselem1  45795  climsuse  45796  limsupresico  45886  limsupubuzlem  45898  limsupmnfuzlem  45912  limsupre3uzlem  45921  liminfresico  45957  limsup10exlem  45958  cnrefiisplem  46015  dvdivbd  46109  dvbdfbdioolem2  46115  ioodvbdlimc1lem1  46117  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnmul  46129  dvnprodlem1  46132  dvnprodlem2  46133  iblspltprt  46159  itgspltprt  46165  stoweidlem1  46187  stoweidlem3  46189  stoweidlem5  46191  stoweidlem11  46197  stoweidlem17  46203  stoweidlem20  46206  stoweidlem26  46212  stoweidlem34  46220  wallispilem4  46254  stirlinglem11  46270  stirlinglem12  46271  stirlinglem13  46272  fourierdlem12  46305  fourierdlem15  46308  fourierdlem20  46313  fourierdlem30  46323  fourierdlem39  46332  fourierdlem42  46335  fourierdlem47  46339  fourierdlem50  46342  fourierdlem64  46356  fourierdlem65  46357  fourierdlem68  46360  fourierdlem73  46365  fourierdlem77  46369  fourierdlem79  46371  fourierdlem87  46379  elaa2lem  46419  etransclem23  46443  ioorrnopnlem  46490  salgencntex  46529  sge0le  46593  sge0isum  46613  sge0xaddlem1  46619  hoicvr  46734  hsphoidmvle2  46771  hoidmv1lelem1  46777  hoidmv1lelem2  46778  hoidmv1lelem3  46779  hoidmvlelem1  46781  hoidmvlelem2  46782  hoidmvlelem4  46784  hspmbllem1  46812  hspmbllem2  46813  smfmullem1  46977  smfmullem2  46978  smfmullem3  46979  smfsuplem1  46997  ormkglobd  47061  natglobalincr  47063  2ltceilhalf  47516  ceilhalfnn  47524  modmknepk  47550  lighneallem4a  47796  gpgusgralem  48244  gpgedgvtx1  48250  gpg3kgrtriexlem4  48274  gpg3kgrtriexlem6  48276  fllog2  48756  itcovalt2lem2lem1  48861