Theorem letrd 11141

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2107   class class class wbr 5075  ℝcr 10879   ≤ cle 11019

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 2710  ax-sep 5224  ax-nul 5231  ax-pow 5289  ax-pr 5353  ax-un 7597  ax-resscn 10937  ax-pre-lttri 10954  ax-pre-lttrn 10955

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-nel 3051  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-pw 4536  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445  df-er 8507  df-en 8743  df-dom 8744  df-sdom 8745  df-pnf 11020  df-mnf 11021  df-xr 11022  df-ltxr 11023  df-le 11024

This theorem is referenced by:  lesub3d  11602  supmul1  11953  supmul  11956  nn0negleid  12294  eluzuzle  12600  iccsplit  13226  supicc  13242  fzdisj  13292  ssfzunsnext  13310  difelfzle  13378  flwordi  13541  flleceil  13582  uzsup  13592  modltm1p1mod  13652  seqf1olem1  13771  bernneq  13953  bernneq3  13955  discr1  13963  faclbnd  14013  faclbnd4lem1  14016  facubnd  14023  seqcoll  14187  sqrlem7  14969  absle  15036  releabs  15042  absrdbnd  15062  rexuzre  15073  limsupgre  15199  lo1bddrp  15243  rlimclim1  15263  rlimresb  15283  rlimrege0  15297  o1add  15332  o1sub  15334  climsqz  15359  climsqz2  15360  rlimsqzlem  15369  rlimsqz  15370  rlimsqz2  15371  rlimno1  15374  isercoll  15388  caucvgrlem  15393  iseraltlem3  15404  o1fsum  15534  cvgcmp  15537  cvgcmpce  15539  climcnds  15572  expcnv  15585  cvgrat  15604  mertenslem2  15606  fprodle  15715  eftlub  15827  rpnnen2lem12  15943  bitsfzo  16151  isprm5  16421  isprm7  16422  eulerthlem2  16492  pcmpt2  16603  pcfac  16609  prmreclem3  16628  prmreclem4  16629  prmreclem5  16630  4sqlem11  16665  vdwlem1  16691  vdwlem3  16693  setsstruct2  16884  prdsxmetlem  23530  nrmmetd  23739  nm2dif  23790  nlmvscnlem2  23858  nmoco  23910  nmotri  23912  nghmcn  23918  icccmplem2  23995  reconnlem2  23999  elii1  24107  xrhmeo  24118  cnheiborlem  24126  bndth  24130  tcphcphlem1  24408  ipcnlem2  24417  cncmet  24495  trirn  24573  minveclem2  24599  minveclem4  24605  ivthlem2  24625  ovolunlem1a  24669  ovolunlem1  24670  ovolfiniun  24674  ovoliunlem1  24675  ovolicc2lem4  24693  ovolicc2lem5  24694  ovolicopnf  24697  nulmbl2  24709  ioombl1lem4  24734  ioorcl2  24745  uniioombllem3  24758  uniioombllem4  24759  uniioombllem5  24760  volcn  24779  vitalilem2  24782  vitali  24786  mbfi1fseqlem5  24893  mbfi1fseqlem6  24894  itg2splitlem  24922  itg2monolem1  24924  itg2monolem3  24926  itg2mono  24927  itg2cnlem1  24935  itgle  24983  bddmulibl  25012  bddiblnc  25015  ditgsplitlem  25033  dveflem  25152  dvlip  25166  dveq0  25173  dvfsumabs  25196  dvfsumlem1  25199  dvfsumlem2  25200  dvfsumlem3  25201  dvfsumlem4  25202  dvfsum2  25207  fta1glem2  25340  dgradd2  25438  plydiveu  25467  fta1lem  25476  aalioulem2  25502  aalioulem3  25503  aalioulem4  25504  aalioulem5  25505  aaliou3lem8  25514  aaliou3lem9  25519  ulmbdd  25566  ulmcn  25567  mtest  25572  mtestbdd  25573  abelthlem2  25600  abelthlem7  25606  pilem2  25620  tanabsge  25672  cosordlem  25695  tanord  25703  logneg2  25779  abslogle  25782  dvlog2lem  25816  cxple2a  25863  abscxpbnd  25915  atans2  26090  leibpi  26101  o1cxp  26133  cxploglim2  26137  jensenlem2  26146  emcllem6  26159  harmoniclbnd  26167  harmonicubnd  26168  harmonicbnd4  26169  fsumharmonic  26170  lgamgulmlem2  26188  lgamgulmlem3  26189  lgamgulmlem5  26191  lgambdd  26195  ftalem2  26232  basellem3  26241  basellem5  26243  basellem6  26244  dvdsflsumcom  26346  fsumfldivdiaglem  26347  ppiub  26361  chtublem  26368  logfac2  26374  chpub  26377  logfacubnd  26378  logfaclbnd  26379  logfacbnd3  26380  logexprlim  26382  bcmono  26434  bpos1lem  26439  bposlem1  26441  bposlem2  26442  bposlem3  26443  bposlem4  26444  bposlem5  26445  bposlem6  26446  bposlem7  26447  bposlem9  26449  lgsdirprm  26488  lgsquadlem1  26537  2lgslem1c  26550  2sqlem8  26583  chebbnd1lem1  26626  chebbnd1lem3  26628  chtppilimlem1  26630  chpchtlim  26636  vmadivsumb  26640  rplogsumlem1  26641  rplogsumlem2  26642  rpvmasumlem  26644  dchrisumlema  26645  dchrisumlem2  26647  dchrisumlem3  26648  dchrmusum2  26651  dchrvmasumlem2  26655  dchrvmasumlem3  26656  dchrvmasumlema  26657  dchrvmasumiflem1  26658  dchrisum0flblem1  26665  dchrisum0flblem2  26666  dchrisum0fno1  26668  dchrisum0re  26670  dchrisum0lem1b  26672  dchrisum0lem1  26673  dchrisum0lem2a  26674  dchrisum0  26677  rplogsum  26684  mudivsum  26687  mulogsumlem  26688  logdivsum  26690  mulog2sumlem1  26691  mulog2sumlem2  26692  2vmadivsumlem  26697  log2sumbnd  26701  selberglem2  26703  selbergb  26706  selberg2lem  26707  selberg2b  26709  chpdifbndlem1  26710  logdivbnd  26713  selberg3lem1  26714  selberg3lem2  26715  selberg4lem1  26717  pntrmax  26721  pntrsumo1  26722  pntrsumbnd  26723  pntrlog2bndlem1  26734  pntrlog2bndlem2  26735  pntrlog2bndlem3  26736  pntrlog2bndlem5  26738  pntrlog2bndlem6  26740  pntrlog2bnd  26741  pntpbnd1a  26742  pntpbnd1  26743  pntpbnd2  26744  pntibndlem2  26748  pntibndlem3  26749  pntlemg  26755  pntlemr  26759  pntlemj  26760  pntlemf  26762  pntlemk  26763  pntlemo  26764  pntleml  26768  abvcxp  26772  qabvle  26782  padicabv  26787  ostth2lem2  26791  ostth2lem3  26792  ostth3  26795  axlowdimlem16  27334  axcontlem8  27348  axcontlem10  27350  wwlksm1edg  28255  wwlksubclwwlk  28431  smcnlem  29068  nmoub3i  29144  ubthlem3  29243  minvecolem2  29246  minvecolem3  29247  minvecolem4  29251  htthlem  29288  bcs2  29553  pjhthlem1  29762  cnlnadjlem2  30439  cnlnadjlem7  30444  nmopadjlem  30460  nmoptrii  30465  nmopcoadji  30472  leopnmid  30509  cdj1i  30804  nndiffz1  31116  pmtrto1cl  31375  psgnfzto1stlem  31376  fzto1st  31379  psgnfzto1st  31381  cyc3conja  31433  smatrcl  31755  submateqlem1  31766  nexple  31986  esumpcvgval  32055  oddpwdc  32330  eulerpartlems  32336  eulerpartlemgc  32338  eulerpartlemb  32344  dstfrvunirn  32450  orvclteinc  32451  ballotlemsima  32491  ballotlemfrcn0  32505  signstfveq0  32565  fsum2dsub  32596  breprexplemc  32621  breprexp  32622  logdivsqrle  32639  hgt750lemb  32645  hgt750leme  32647  tgoldbachgnn  32648  dnibndlem2  34668  dnibndlem6  34672  dnibndlem9  34675  dnibndlem10  34676  dnibndlem11  34677  dnibndlem12  34678  knoppcnlem4  34685  unblimceq0lem  34695  unblimceq0  34696  unbdqndv2lem2  34699  knoppndvlem11  34711  knoppndvlem14  34714  knoppndvlem15  34715  knoppndvlem18  34718  knoppndvlem21  34721  poimirlem6  35792  poimirlem7  35793  poimirlem13  35799  poimirlem15  35801  poimirlem29  35815  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  itg2addnc  35840  iblmulc2nc  35851  ftc1anclem7  35865  ftc1anclem8  35866  filbcmb  35907  geomcau  35926  prdsbnd  35960  cntotbnd  35963  bfplem2  35990  rrntotbnd  36003  iccbnd  36007  lcmineqlem20  40063  lcmineqlem21  40064  lcmineqlem22  40065  3lexlogpow5ineq2  40070  3lexlogpow5ineq5  40075  aks4d1p1p2  40085  aks4d1p1p4  40086  aks4d1p1p7  40089  aks4d1p1p5  40090  aks4d1p1  40091  aks4d1p2  40092  aks4d1p3  40093  aks4d1p5  40095  aks4d1p6  40096  aks4d1p7d1  40097  aks4d1p7  40098  aks4d1p8  40102  2np3bcnp1  40107  sticksstones6  40114  sticksstones7  40115  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  sticksstones22  40131  metakunt1  40132  metakunt12  40143  metakunt28  40159  lzunuz  40597  irrapxlem3  40653  irrapxlem4  40654  irrapxlem5  40655  pellexlem2  40659  pell1qrge1  40699  monotoddzzfi  40771  jm2.17a  40789  rmygeid  40793  fzmaxdif  40810  jm2.27c  40836  jm3.1lem1  40846  expdiophlem1  40850  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  imo72b2lem0  41783  int-ineqtransd  41812  dvgrat  41937  monoords  42843  absnpncan2d  42848  absnpncan3d  42853  ssfiunibd  42855  leadd12dd  42862  rexabslelem  42965  uzublem  42977  sqrlearg  43098  fmul01  43128  fmul01lt1lem1  43132  fmul01lt1lem2  43133  climsuselem1  43155  climsuse  43156  limsupresico  43248  limsupubuzlem  43260  limsupmnfuzlem  43274  limsupre3uzlem  43283  liminfresico  43319  limsup10exlem  43320  cnrefiisplem  43377  dvdivbd  43471  dvbdfbdioolem2  43477  ioodvbdlimc1lem1  43479  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnmul  43491  dvnprodlem1  43494  dvnprodlem2  43495  iblspltprt  43521  itgspltprt  43527  stoweidlem1  43549  stoweidlem3  43551  stoweidlem5  43553  stoweidlem11  43559  stoweidlem17  43565  stoweidlem20  43568  stoweidlem26  43574  stoweidlem34  43582  wallispilem4  43616  stirlinglem11  43632  stirlinglem12  43633  stirlinglem13  43634  fourierdlem12  43667  fourierdlem15  43670  fourierdlem20  43675  fourierdlem30  43685  fourierdlem39  43694  fourierdlem42  43697  fourierdlem47  43701  fourierdlem50  43704  fourierdlem64  43718  fourierdlem65  43719  fourierdlem68  43722  fourierdlem73  43727  fourierdlem77  43731  fourierdlem79  43733  fourierdlem87  43741  elaa2lem  43781  etransclem23  43805  ioorrnopnlem  43852  salgencntex  43889  sge0le  43952  sge0isum  43972  sge0xaddlem1  43978  hoicvr  44093  hsphoidmvle2  44130  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  hoidmvlelem1  44140  hoidmvlelem2  44141  hoidmvlelem4  44143  hspmbllem1  44171  hspmbllem2  44172  smfmullem1  44336  smfmullem2  44337  smfmullem3  44338  smfsuplem1  44355  lighneallem4a  45071  fllog2  45925  itcovalt2lem2lem1  46030  natglobalincr  46523