Theorem letrd 11390

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5119  ℝcr 11126   ≤ cle 11268

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7727  ax-resscn 11184  ax-pre-lttri 11201  ax-pre-lttrn 11202

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-nel 3037  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-f1 6535  df-fo 6536  df-f1o 6537  df-fv 6538  df-er 8717  df-en 8958  df-dom 8959  df-sdom 8960  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273

This theorem is referenced by:  lesub3d  11853  le2addd  11854  supmul1  12209  supmul  12212  nn0negleid  12551  eluzuzle  12859  iccsplit  13500  supicc  13516  fzdisj  13566  ssfzunsnext  13584  difelfzle  13656  flwordi  13827  flleceil  13868  uzsup  13878  modltm1p1mod  13939  seqf1olem1  14057  zzlesq  14222  bernneq  14245  bernneq3  14247  discr1  14255  faclbnd  14306  faclbnd4lem1  14309  facubnd  14316  seqcoll  14480  01sqrexlem7  15265  absle  15332  releabs  15338  absrdbnd  15358  rexuzre  15369  limsupgre  15495  lo1bddrp  15539  rlimclim1  15559  rlimresb  15579  rlimrege0  15593  o1add  15628  o1sub  15630  climsqz  15655  climsqz2  15656  rlimsqzlem  15663  rlimsqz  15664  rlimsqz2  15665  rlimno1  15668  isercoll  15682  caucvgrlem  15687  iseraltlem3  15698  o1fsum  15827  cvgcmp  15830  cvgcmpce  15832  climcnds  15865  expcnv  15878  cvgrat  15897  mertenslem2  15899  fprodle  16010  eftlub  16125  rpnnen2lem12  16241  bitsfzo  16452  isprm5  16724  isprm7  16725  eulerthlem2  16799  pcmpt2  16911  pcfac  16917  prmreclem3  16936  prmreclem4  16937  prmreclem5  16938  4sqlem11  16973  vdwlem1  16999  vdwlem3  17001  setsstruct2  17191  prdsxmetlem  24305  nrmmetd  24511  nm2dif  24562  nlmvscnlem2  24622  nmoco  24674  nmotri  24676  nghmcn  24682  icccmplem2  24761  reconnlem2  24765  elii1  24880  xrhmeo  24893  cnheiborlem  24902  bndth  24906  tcphcphlem1  25185  ipcnlem2  25194  cncmet  25272  trirn  25350  minveclem2  25376  minveclem4  25382  ivthlem2  25403  ovolunlem1a  25447  ovolunlem1  25448  ovolfiniun  25452  ovoliunlem1  25453  ovolicc2lem4  25471  ovolicc2lem5  25472  ovolicopnf  25475  nulmbl2  25487  ioombl1lem4  25512  ioorcl2  25523  uniioombllem3  25536  uniioombllem4  25537  uniioombllem5  25538  volcn  25557  vitalilem2  25560  vitali  25564  mbfi1fseqlem5  25670  mbfi1fseqlem6  25671  itg2splitlem  25699  itg2monolem1  25701  itg2monolem3  25703  itg2mono  25704  itg2cnlem1  25712  itgle  25761  bddmulibl  25790  bddiblnc  25793  ditgsplitlem  25811  dveflem  25933  dvlip  25948  dveq0  25955  dvfsumabs  25979  dvfsumlem1  25982  dvfsumlem2  25983  dvfsumlem2OLD  25984  dvfsumlem3  25985  dvfsumlem4  25986  dvfsum2  25991  fta1glem2  26124  dgradd2  26224  plydiveu  26256  fta1lem  26265  aalioulem2  26291  aalioulem3  26292  aalioulem4  26293  aalioulem5  26294  aaliou3lem8  26303  aaliou3lem9  26308  ulmbdd  26357  ulmcn  26358  mtest  26363  mtestbdd  26364  abelthlem2  26392  abelthlem7  26398  pilem2  26412  tanabsge  26465  cosordlem  26489  tanord  26497  logneg2  26574  abslogle  26577  dvlog2lem  26611  cxple2a  26658  abscxpbnd  26713  atans2  26891  leibpi  26902  o1cxp  26935  cxploglim2  26939  jensenlem2  26948  emcllem6  26961  harmoniclbnd  26969  harmonicubnd  26970  harmonicbnd4  26971  fsumharmonic  26972  lgamgulmlem2  26990  lgamgulmlem3  26991  lgamgulmlem5  26993  lgambdd  26997  ftalem2  27034  basellem3  27043  basellem5  27045  basellem6  27046  dvdsflsumcom  27148  fsumfldivdiaglem  27149  ppiub  27165  chtublem  27172  logfac2  27178  chpub  27181  logfacubnd  27182  logfaclbnd  27183  logfacbnd3  27184  logexprlim  27186  bcmono  27238  bpos1lem  27243  bposlem1  27245  bposlem2  27246  bposlem3  27247  bposlem4  27248  bposlem5  27249  bposlem6  27250  bposlem7  27251  bposlem9  27253  lgsdirprm  27292  lgsquadlem1  27341  2lgslem1c  27354  2sqlem8  27387  chebbnd1lem1  27430  chebbnd1lem3  27432  chtppilimlem1  27434  chpchtlim  27440  vmadivsumb  27444  rplogsumlem1  27445  rplogsumlem2  27446  rpvmasumlem  27448  dchrisumlema  27449  dchrisumlem2  27451  dchrisumlem3  27452  dchrmusum2  27455  dchrvmasumlem2  27459  dchrvmasumlem3  27460  dchrvmasumlema  27461  dchrvmasumiflem1  27462  dchrisum0flblem1  27469  dchrisum0flblem2  27470  dchrisum0fno1  27472  dchrisum0re  27474  dchrisum0lem1b  27476  dchrisum0lem1  27477  dchrisum0lem2a  27478  dchrisum0  27481  rplogsum  27488  mudivsum  27491  mulogsumlem  27492  logdivsum  27494  mulog2sumlem1  27495  mulog2sumlem2  27496  2vmadivsumlem  27501  log2sumbnd  27505  selberglem2  27507  selbergb  27510  selberg2lem  27511  selberg2b  27513  chpdifbndlem1  27514  logdivbnd  27517  selberg3lem1  27518  selberg3lem2  27519  selberg4lem1  27521  pntrmax  27525  pntrsumo1  27526  pntrsumbnd  27527  pntrlog2bndlem1  27538  pntrlog2bndlem2  27539  pntrlog2bndlem3  27540  pntrlog2bndlem5  27542  pntrlog2bndlem6  27544  pntrlog2bnd  27545  pntpbnd1a  27546  pntpbnd1  27547  pntpbnd2  27548  pntibndlem2  27552  pntibndlem3  27553  pntlemg  27559  pntlemr  27563  pntlemj  27564  pntlemf  27566  pntlemk  27567  pntlemo  27568  pntleml  27572  abvcxp  27576  qabvle  27586  padicabv  27591  ostth2lem2  27595  ostth2lem3  27596  ostth3  27599  axlowdimlem16  28882  axcontlem8  28896  axcontlem10  28898  wwlksm1edg  29809  wwlksubclwwlk  29985  smcnlem  30624  nmoub3i  30700  ubthlem3  30799  minvecolem2  30802  minvecolem3  30803  minvecolem4  30807  htthlem  30844  bcs2  31109  pjhthlem1  31318  cnlnadjlem2  31995  cnlnadjlem7  32000  nmopadjlem  32016  nmoptrii  32021  nmopcoadji  32028  leopnmid  32065  cdj1i  32360  nndiffz1  32709  nexple  32769  oexpled  32772  pmtrto1cl  33056  psgnfzto1stlem  33057  fzto1st  33060  psgnfzto1st  33062  cyc3conja  33114  constrresqrtcl  33757  cos9thpiminplylem1  33762  smatrcl  33773  submateqlem1  33784  esumpcvgval  34055  oddpwdc  34332  eulerpartlems  34338  eulerpartlemgc  34340  eulerpartlemb  34346  dstfrvunirn  34453  orvclteinc  34454  ballotlemsima  34494  ballotlemfrcn0  34508  signstfveq0  34555  fsum2dsub  34585  breprexplemc  34610  breprexp  34611  logdivsqrle  34628  hgt750lemb  34634  hgt750leme  34636  tgoldbachgnn  34637  dnibndlem2  36443  dnibndlem6  36447  dnibndlem9  36450  dnibndlem10  36451  dnibndlem11  36452  dnibndlem12  36453  knoppcnlem4  36460  unblimceq0lem  36470  unblimceq0  36471  unbdqndv2lem2  36474  knoppndvlem11  36486  knoppndvlem14  36489  knoppndvlem15  36490  knoppndvlem18  36493  knoppndvlem21  36496  poimirlem6  37596  poimirlem7  37597  poimirlem13  37603  poimirlem15  37605  poimirlem29  37619  mblfinlem2  37628  mblfinlem3  37629  mblfinlem4  37630  ismblfin  37631  itg2addnc  37644  iblmulc2nc  37655  ftc1anclem7  37669  ftc1anclem8  37670  filbcmb  37710  geomcau  37729  prdsbnd  37763  cntotbnd  37766  bfplem2  37793  rrntotbnd  37806  iccbnd  37810  lcmineqlem20  42007  lcmineqlem21  42008  lcmineqlem22  42009  3lexlogpow5ineq2  42014  3lexlogpow5ineq5  42019  aks4d1p1p2  42029  aks4d1p1p4  42030  aks4d1p1p7  42033  aks4d1p1p5  42034  aks4d1p1  42035  aks4d1p2  42036  aks4d1p3  42037  aks4d1p5  42039  aks4d1p6  42040  aks4d1p7d1  42041  aks4d1p7  42042  aks4d1p8  42046  posbezout  42059  aks6d1c1  42075  aks6d1c2lem4  42086  2np3bcnp1  42103  sticksstones6  42110  sticksstones7  42111  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  sticksstones22  42127  bcled  42137  bcle2d  42138  aks6d1c7lem1  42139  aks6d1c7lem2  42140  unitscyglem4  42157  metakunt1  42164  metakunt12  42175  metakunt28  42191  lzunuz  42738  irrapxlem3  42794  irrapxlem4  42795  irrapxlem5  42796  pellexlem2  42800  pell1qrge1  42840  monotoddzzfi  42913  jm2.17a  42931  rmygeid  42935  fzmaxdif  42952  jm2.27c  42978  jm3.1lem1  42988  expdiophlem1  42992  fzunt  43426  fzuntd  43427  fzunt1d  43428  fzuntgd  43429  imo72b2lem0  44136  int-ineqtransd  44165  dvgrat  44284  monoords  45274  absnpncan2d  45279  absnpncan3d  45284  ssfiunibd  45286  rexabslelem  45393  uzublem  45405  sqrlearg  45530  fmul01  45557  fmul01lt1lem1  45561  fmul01lt1lem2  45562  climsuselem1  45584  climsuse  45585  limsupresico  45677  limsupubuzlem  45689  limsupmnfuzlem  45703  limsupre3uzlem  45712  liminfresico  45748  limsup10exlem  45749  cnrefiisplem  45806  dvdivbd  45900  dvbdfbdioolem2  45906  ioodvbdlimc1lem1  45908  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnmul  45920  dvnprodlem1  45923  dvnprodlem2  45924  iblspltprt  45950  itgspltprt  45956  stoweidlem1  45978  stoweidlem3  45980  stoweidlem5  45982  stoweidlem11  45988  stoweidlem17  45994  stoweidlem20  45997  stoweidlem26  46003  stoweidlem34  46011  wallispilem4  46045  stirlinglem11  46061  stirlinglem12  46062  stirlinglem13  46063  fourierdlem12  46096  fourierdlem15  46099  fourierdlem20  46104  fourierdlem30  46114  fourierdlem39  46123  fourierdlem42  46126  fourierdlem47  46130  fourierdlem50  46133  fourierdlem64  46147  fourierdlem65  46148  fourierdlem68  46151  fourierdlem73  46156  fourierdlem77  46160  fourierdlem79  46162  fourierdlem87  46170  elaa2lem  46210  etransclem23  46234  ioorrnopnlem  46281  salgencntex  46320  sge0le  46384  sge0isum  46404  sge0xaddlem1  46410  hoicvr  46525  hsphoidmvle2  46562  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1lelem3  46570  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem4  46575  hspmbllem1  46603  hspmbllem2  46604  smfmullem1  46768  smfmullem2  46769  smfmullem3  46770  smfsuplem1  46788  ormkglobd  46852  natglobalincr  46854  2ltceilhalf  47305  ceilhalfnn  47313  lighneallem4a  47570  gpgusgralem  48008  gpgedgvtx1  48014  gpg3nbgrvtxlem  48017  gpg3kgrtriexlem4  48036  gpg3kgrtriexlem6  48038  fllog2  48496  itcovalt2lem2lem1  48601