Theorem letrd 11062

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5070  ℝcr 10801   ≤ cle 10941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-resscn 10859  ax-pre-lttri 10876  ax-pre-lttrn 10877

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946

This theorem is referenced by:  lesub3d  11523  supmul1  11874  supmul  11877  nn0negleid  12215  eluzuzle  12520  iccsplit  13146  supicc  13162  fzdisj  13212  ssfzunsnext  13230  difelfzle  13298  flwordi  13460  flleceil  13501  uzsup  13511  modltm1p1mod  13571  seqf1olem1  13690  bernneq  13872  bernneq3  13874  discr1  13882  faclbnd  13932  faclbnd4lem1  13935  facubnd  13942  seqcoll  14106  sqrlem7  14888  absle  14955  releabs  14961  absrdbnd  14981  rexuzre  14992  limsupgre  15118  lo1bddrp  15162  rlimclim1  15182  rlimresb  15202  rlimrege0  15216  o1add  15251  o1sub  15253  climsqz  15278  climsqz2  15279  rlimsqzlem  15288  rlimsqz  15289  rlimsqz2  15290  rlimno1  15293  isercoll  15307  caucvgrlem  15312  iseraltlem3  15323  o1fsum  15453  cvgcmp  15456  cvgcmpce  15458  climcnds  15491  expcnv  15504  cvgrat  15523  mertenslem2  15525  fprodle  15634  eftlub  15746  rpnnen2lem12  15862  bitsfzo  16070  isprm5  16340  isprm7  16341  eulerthlem2  16411  pcmpt2  16522  pcfac  16528  prmreclem3  16547  prmreclem4  16548  prmreclem5  16549  4sqlem11  16584  vdwlem1  16610  vdwlem3  16612  setsstruct2  16803  prdsxmetlem  23429  nrmmetd  23636  nm2dif  23687  nlmvscnlem2  23755  nmoco  23807  nmotri  23809  nghmcn  23815  icccmplem2  23892  reconnlem2  23896  elii1  24004  xrhmeo  24015  cnheiborlem  24023  bndth  24027  tcphcphlem1  24304  ipcnlem2  24313  cncmet  24391  trirn  24469  minveclem2  24495  minveclem4  24501  ivthlem2  24521  ovolunlem1a  24565  ovolunlem1  24566  ovolfiniun  24570  ovoliunlem1  24571  ovolicc2lem4  24589  ovolicc2lem5  24590  ovolicopnf  24593  nulmbl2  24605  ioombl1lem4  24630  ioorcl2  24641  uniioombllem3  24654  uniioombllem4  24655  uniioombllem5  24656  volcn  24675  vitalilem2  24678  vitali  24682  mbfi1fseqlem5  24789  mbfi1fseqlem6  24790  itg2splitlem  24818  itg2monolem1  24820  itg2monolem3  24822  itg2mono  24823  itg2cnlem1  24831  itgle  24879  bddmulibl  24908  bddiblnc  24911  ditgsplitlem  24929  dveflem  25048  dvlip  25062  dveq0  25069  dvfsumabs  25092  dvfsumlem1  25095  dvfsumlem2  25096  dvfsumlem3  25097  dvfsumlem4  25098  dvfsum2  25103  fta1glem2  25236  dgradd2  25334  plydiveu  25363  fta1lem  25372  aalioulem2  25398  aalioulem3  25399  aalioulem4  25400  aalioulem5  25401  aaliou3lem8  25410  aaliou3lem9  25415  ulmbdd  25462  ulmcn  25463  mtest  25468  mtestbdd  25469  abelthlem2  25496  abelthlem7  25502  pilem2  25516  tanabsge  25568  cosordlem  25591  tanord  25599  logneg2  25675  abslogle  25678  dvlog2lem  25712  cxple2a  25759  abscxpbnd  25811  atans2  25986  leibpi  25997  o1cxp  26029  cxploglim2  26033  jensenlem2  26042  emcllem6  26055  harmoniclbnd  26063  harmonicubnd  26064  harmonicbnd4  26065  fsumharmonic  26066  lgamgulmlem2  26084  lgamgulmlem3  26085  lgamgulmlem5  26087  lgambdd  26091  ftalem2  26128  basellem3  26137  basellem5  26139  basellem6  26140  dvdsflsumcom  26242  fsumfldivdiaglem  26243  ppiub  26257  chtublem  26264  logfac2  26270  chpub  26273  logfacubnd  26274  logfaclbnd  26275  logfacbnd3  26276  logexprlim  26278  bcmono  26330  bpos1lem  26335  bposlem1  26337  bposlem2  26338  bposlem3  26339  bposlem4  26340  bposlem5  26341  bposlem6  26342  bposlem7  26343  bposlem9  26345  lgsdirprm  26384  lgsquadlem1  26433  2lgslem1c  26446  2sqlem8  26479  chebbnd1lem1  26522  chebbnd1lem3  26524  chtppilimlem1  26526  chpchtlim  26532  vmadivsumb  26536  rplogsumlem1  26537  rplogsumlem2  26538  rpvmasumlem  26540  dchrisumlema  26541  dchrisumlem2  26543  dchrisumlem3  26544  dchrmusum2  26547  dchrvmasumlem2  26551  dchrvmasumlem3  26552  dchrvmasumlema  26553  dchrvmasumiflem1  26554  dchrisum0flblem1  26561  dchrisum0flblem2  26562  dchrisum0fno1  26564  dchrisum0re  26566  dchrisum0lem1b  26568  dchrisum0lem1  26569  dchrisum0lem2a  26570  dchrisum0  26573  rplogsum  26580  mudivsum  26583  mulogsumlem  26584  logdivsum  26586  mulog2sumlem1  26587  mulog2sumlem2  26588  2vmadivsumlem  26593  log2sumbnd  26597  selberglem2  26599  selbergb  26602  selberg2lem  26603  selberg2b  26605  chpdifbndlem1  26606  logdivbnd  26609  selberg3lem1  26610  selberg3lem2  26611  selberg4lem1  26613  pntrmax  26617  pntrsumo1  26618  pntrsumbnd  26619  pntrlog2bndlem1  26630  pntrlog2bndlem2  26631  pntrlog2bndlem3  26632  pntrlog2bndlem5  26634  pntrlog2bndlem6  26636  pntrlog2bnd  26637  pntpbnd1a  26638  pntpbnd1  26639  pntpbnd2  26640  pntibndlem2  26644  pntibndlem3  26645  pntlemg  26651  pntlemr  26655  pntlemj  26656  pntlemf  26658  pntlemk  26659  pntlemo  26660  pntleml  26664  abvcxp  26668  qabvle  26678  padicabv  26683  ostth2lem2  26687  ostth2lem3  26688  ostth3  26691  axlowdimlem16  27228  axcontlem8  27242  axcontlem10  27244  wwlksm1edg  28147  wwlksubclwwlk  28323  smcnlem  28960  nmoub3i  29036  ubthlem3  29135  minvecolem2  29138  minvecolem3  29139  minvecolem4  29143  htthlem  29180  bcs2  29445  pjhthlem1  29654  cnlnadjlem2  30331  cnlnadjlem7  30336  nmopadjlem  30352  nmoptrii  30357  nmopcoadji  30364  leopnmid  30401  cdj1i  30696  nndiffz1  31009  pmtrto1cl  31268  psgnfzto1stlem  31269  fzto1st  31272  psgnfzto1st  31274  cyc3conja  31326  smatrcl  31648  submateqlem1  31659  nexple  31877  esumpcvgval  31946  oddpwdc  32221  eulerpartlems  32227  eulerpartlemgc  32229  eulerpartlemb  32235  dstfrvunirn  32341  orvclteinc  32342  ballotlemsima  32382  ballotlemfrcn0  32396  signstfveq0  32456  fsum2dsub  32487  breprexplemc  32512  breprexp  32513  logdivsqrle  32530  hgt750lemb  32536  hgt750leme  32538  tgoldbachgnn  32539  dnibndlem2  34586  dnibndlem6  34590  dnibndlem9  34593  dnibndlem10  34594  dnibndlem11  34595  dnibndlem12  34596  knoppcnlem4  34603  unblimceq0lem  34613  unblimceq0  34614  unbdqndv2lem2  34617  knoppndvlem11  34629  knoppndvlem14  34632  knoppndvlem15  34633  knoppndvlem18  34636  knoppndvlem21  34639  poimirlem6  35710  poimirlem7  35711  poimirlem13  35717  poimirlem15  35719  poimirlem29  35733  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  itg2addnc  35758  iblmulc2nc  35769  ftc1anclem7  35783  ftc1anclem8  35784  filbcmb  35825  geomcau  35844  prdsbnd  35878  cntotbnd  35881  bfplem2  35908  rrntotbnd  35921  iccbnd  35925  lcmineqlem20  39984  lcmineqlem21  39985  lcmineqlem22  39986  3lexlogpow5ineq2  39991  3lexlogpow5ineq5  39996  aks4d1p1p2  40006  aks4d1p1p4  40007  aks4d1p1p7  40010  aks4d1p1p5  40011  aks4d1p1  40012  aks4d1p2  40013  aks4d1p3  40014  aks4d1p5  40016  aks4d1p6  40017  aks4d1p7d1  40018  aks4d1p7  40019  aks4d1p8  40023  2np3bcnp1  40028  sticksstones6  40035  sticksstones7  40036  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  sticksstones22  40052  metakunt1  40053  metakunt12  40064  metakunt28  40080  lzunuz  40506  irrapxlem3  40562  irrapxlem4  40563  irrapxlem5  40564  pellexlem2  40568  pell1qrge1  40608  monotoddzzfi  40680  jm2.17a  40698  rmygeid  40702  fzmaxdif  40719  jm2.27c  40745  jm3.1lem1  40755  expdiophlem1  40759  imo72b2lem0  41665  int-ineqtransd  41694  dvgrat  41819  monoords  42726  absnpncan2d  42731  absnpncan3d  42736  ssfiunibd  42738  leadd12dd  42745  rexabslelem  42848  uzublem  42860  sqrlearg  42981  fmul01  43011  fmul01lt1lem1  43015  fmul01lt1lem2  43016  climsuselem1  43038  climsuse  43039  limsupresico  43131  limsupubuzlem  43143  limsupmnfuzlem  43157  limsupre3uzlem  43166  liminfresico  43202  limsup10exlem  43203  cnrefiisplem  43260  dvdivbd  43354  dvbdfbdioolem2  43360  ioodvbdlimc1lem1  43362  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnmul  43374  dvnprodlem1  43377  dvnprodlem2  43378  iblspltprt  43404  itgspltprt  43410  stoweidlem1  43432  stoweidlem3  43434  stoweidlem5  43436  stoweidlem11  43442  stoweidlem17  43448  stoweidlem20  43451  stoweidlem26  43457  stoweidlem34  43465  wallispilem4  43499  stirlinglem11  43515  stirlinglem12  43516  stirlinglem13  43517  fourierdlem12  43550  fourierdlem15  43553  fourierdlem20  43558  fourierdlem30  43568  fourierdlem39  43577  fourierdlem42  43580  fourierdlem47  43584  fourierdlem50  43587  fourierdlem64  43601  fourierdlem65  43602  fourierdlem68  43605  fourierdlem73  43610  fourierdlem77  43614  fourierdlem79  43616  fourierdlem87  43624  elaa2lem  43664  etransclem23  43688  ioorrnopnlem  43735  salgencntex  43772  sge0le  43835  sge0isum  43855  sge0xaddlem1  43861  hoicvr  43976  hsphoidmvle2  44013  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem4  44026  hspmbllem1  44054  hspmbllem2  44055  smfmullem1  44212  smfmullem2  44213  smfmullem3  44214  smfsuplem1  44231  lighneallem4a  44948  fllog2  45802  itcovalt2lem2lem1  45907