Theorem letrd 10797

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114   class class class wbr 5066  ℝcr 10536   ≤ cle 10676

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-resscn 10594  ax-pre-lttri 10611  ax-pre-lttrn 10612

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-mpt 5147  df-id 5460  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-er 8289  df-en 8510  df-dom 8511  df-sdom 8512  df-pnf 10677  df-mnf 10678  df-xr 10679  df-ltxr 10680  df-le 10681

This theorem is referenced by:  lesub3d  11258  supmul1  11610  supmul  11613  nn0negleid  11950  eluzuzle  12253  iccsplit  12872  supicc  12887  fzdisj  12935  ssfzunsnext  12953  difelfzle  13021  flwordi  13183  flleceil  13222  uzsup  13232  modltm1p1mod  13292  seqf1olem1  13410  bernneq  13591  bernneq3  13593  discr1  13601  faclbnd  13651  faclbnd4lem1  13654  facubnd  13661  seqcoll  13823  sqrlem7  14608  absle  14675  releabs  14681  absrdbnd  14701  rexuzre  14712  limsupgre  14838  lo1bddrp  14882  rlimclim1  14902  rlimresb  14922  rlimrege0  14936  o1add  14970  o1sub  14972  climsqz  14997  climsqz2  14998  rlimsqzlem  15005  rlimsqz  15006  rlimsqz2  15007  rlimno1  15010  isercoll  15024  caucvgrlem  15029  iseraltlem3  15040  o1fsum  15168  cvgcmp  15171  cvgcmpce  15173  climcnds  15206  expcnv  15219  cvgrat  15239  mertenslem2  15241  fprodle  15350  eftlub  15462  rpnnen2lem12  15578  bitsfzo  15784  isprm5  16051  isprm7  16052  eulerthlem2  16119  pcmpt2  16229  pcfac  16235  prmreclem3  16254  prmreclem4  16255  prmreclem5  16256  4sqlem11  16291  vdwlem1  16317  vdwlem3  16319  setsstruct2  16521  prdsxmetlem  22978  nrmmetd  23184  nm2dif  23234  nlmvscnlem2  23294  nmoco  23346  nmotri  23348  nghmcn  23354  icccmplem2  23431  reconnlem2  23435  elii1  23539  xrhmeo  23550  cnheiborlem  23558  bndth  23562  tcphcphlem1  23838  ipcnlem2  23847  cncmet  23925  trirn  24003  minveclem2  24029  minveclem4  24035  ivthlem2  24053  ovolunlem1a  24097  ovolunlem1  24098  ovolfiniun  24102  ovoliunlem1  24103  ovolicc2lem4  24121  ovolicc2lem5  24122  ovolicopnf  24125  nulmbl2  24137  ioombl1lem4  24162  ioorcl2  24173  uniioombllem3  24186  uniioombllem4  24187  uniioombllem5  24188  volcn  24207  vitalilem2  24210  vitali  24214  mbfi1fseqlem5  24320  mbfi1fseqlem6  24321  itg2splitlem  24349  itg2monolem1  24351  itg2monolem3  24353  itg2mono  24354  itg2cnlem1  24362  itgle  24410  bddmulibl  24439  ditgsplitlem  24458  dveflem  24576  dvlip  24590  dveq0  24597  dvfsumabs  24620  dvfsumlem1  24623  dvfsumlem2  24624  dvfsumlem3  24625  dvfsumlem4  24626  dvfsum2  24631  fta1glem2  24760  dgradd2  24858  plydiveu  24887  fta1lem  24896  aalioulem2  24922  aalioulem3  24923  aalioulem4  24924  aalioulem5  24925  aaliou3lem8  24934  aaliou3lem9  24939  ulmbdd  24986  ulmcn  24987  mtest  24992  mtestbdd  24993  abelthlem2  25020  abelthlem7  25026  pilem2  25040  tanabsge  25092  cosordlem  25115  tanord  25122  logneg2  25198  abslogle  25201  dvlog2lem  25235  cxple2a  25282  abscxpbnd  25334  atans2  25509  leibpi  25520  o1cxp  25552  cxploglim2  25556  jensenlem2  25565  emcllem6  25578  harmoniclbnd  25586  harmonicubnd  25587  harmonicbnd4  25588  fsumharmonic  25589  lgamgulmlem2  25607  lgamgulmlem3  25608  lgamgulmlem5  25610  lgambdd  25614  ftalem2  25651  basellem3  25660  basellem5  25662  basellem6  25663  dvdsflsumcom  25765  fsumfldivdiaglem  25766  ppiub  25780  chtublem  25787  logfac2  25793  chpub  25796  logfacubnd  25797  logfaclbnd  25798  logfacbnd3  25799  logexprlim  25801  bcmono  25853  bpos1lem  25858  bposlem1  25860  bposlem2  25861  bposlem3  25862  bposlem4  25863  bposlem5  25864  bposlem6  25865  bposlem7  25866  bposlem9  25868  lgsdirprm  25907  lgsquadlem1  25956  2lgslem1c  25969  2sqlem8  26002  chebbnd1lem1  26045  chebbnd1lem3  26047  chtppilimlem1  26049  chpchtlim  26055  vmadivsumb  26059  rplogsumlem1  26060  rplogsumlem2  26061  rpvmasumlem  26063  dchrisumlema  26064  dchrisumlem2  26066  dchrisumlem3  26067  dchrmusum2  26070  dchrvmasumlem2  26074  dchrvmasumlem3  26075  dchrvmasumlema  26076  dchrvmasumiflem1  26077  dchrisum0flblem1  26084  dchrisum0flblem2  26085  dchrisum0fno1  26087  dchrisum0re  26089  dchrisum0lem1b  26091  dchrisum0lem1  26092  dchrisum0lem2a  26093  dchrisum0  26096  rplogsum  26103  mudivsum  26106  mulogsumlem  26107  logdivsum  26109  mulog2sumlem1  26110  mulog2sumlem2  26111  2vmadivsumlem  26116  log2sumbnd  26120  selberglem2  26122  selbergb  26125  selberg2lem  26126  selberg2b  26128  chpdifbndlem1  26129  logdivbnd  26132  selberg3lem1  26133  selberg3lem2  26134  selberg4lem1  26136  pntrmax  26140  pntrsumo1  26141  pntrsumbnd  26142  pntrlog2bndlem1  26153  pntrlog2bndlem2  26154  pntrlog2bndlem3  26155  pntrlog2bndlem5  26157  pntrlog2bndlem6  26159  pntrlog2bnd  26160  pntpbnd1a  26161  pntpbnd1  26162  pntpbnd2  26163  pntibndlem2  26167  pntibndlem3  26168  pntlemg  26174  pntlemr  26178  pntlemj  26179  pntlemf  26181  pntlemk  26182  pntlemo  26183  pntleml  26187  abvcxp  26191  qabvle  26201  padicabv  26206  ostth2lem2  26210  ostth2lem3  26211  ostth3  26214  axlowdimlem16  26743  axcontlem8  26757  axcontlem10  26759  wwlksm1edg  27659  wwlksubclwwlk  27837  smcnlem  28474  nmoub3i  28550  ubthlem3  28649  minvecolem2  28652  minvecolem3  28653  minvecolem4  28657  htthlem  28694  bcs2  28959  pjhthlem1  29168  cnlnadjlem2  29845  cnlnadjlem7  29850  nmopadjlem  29866  nmoptrii  29871  nmopcoadji  29878  leopnmid  29915  cdj1i  30210  nndiffz1  30509  pmtrto1cl  30741  psgnfzto1stlem  30742  fzto1st  30745  psgnfzto1st  30747  cyc3conja  30799  smatrcl  31061  submateqlem1  31072  nexple  31268  esumpcvgval  31337  oddpwdc  31612  eulerpartlems  31618  eulerpartlemgc  31620  eulerpartlemb  31626  dstfrvunirn  31732  orvclteinc  31733  ballotlemsima  31773  ballotlemfrcn0  31787  signstfveq0  31847  fsum2dsub  31878  breprexplemc  31903  breprexp  31904  logdivsqrle  31921  hgt750lemb  31927  hgt750leme  31929  tgoldbachgnn  31930  dnibndlem2  33818  dnibndlem6  33822  dnibndlem9  33825  dnibndlem10  33826  dnibndlem11  33827  dnibndlem12  33828  knoppcnlem4  33835  unblimceq0lem  33845  unblimceq0  33846  unbdqndv2lem2  33849  knoppndvlem11  33861  knoppndvlem14  33864  knoppndvlem15  33865  knoppndvlem18  33868  knoppndvlem21  33871  poimirlem6  34913  poimirlem7  34914  poimirlem13  34920  poimirlem15  34922  poimirlem29  34936  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  itg2addnc  34961  iblmulc2nc  34972  bddiblnc  34977  ftc1anclem7  34988  ftc1anclem8  34989  filbcmb  35030  geomcau  35049  prdsbnd  35086  cntotbnd  35089  bfplem2  35116  rrntotbnd  35129  iccbnd  35133  lzunuz  39414  irrapxlem3  39470  irrapxlem4  39471  irrapxlem5  39472  pellexlem2  39476  pell1qrge1  39516  monotoddzzfi  39588  jm2.17a  39606  rmygeid  39610  fzmaxdif  39627  jm2.27c  39653  jm3.1lem1  39663  expdiophlem1  39667  imo72b2lem0  40565  int-ineqtransd  40596  dvgrat  40693  monoords  41613  absnpncan2d  41618  absnpncan3d  41623  ssfiunibd  41625  leadd12dd  41633  rexabslelem  41741  uzublem  41753  sqrlearg  41878  fmul01  41910  fmul01lt1lem1  41914  fmul01lt1lem2  41915  climsuselem1  41937  climsuse  41938  limsupresico  42030  limsupubuzlem  42042  limsupmnfuzlem  42056  limsupre3uzlem  42065  liminfresico  42101  limsup10exlem  42102  cnrefiisplem  42159  dvdivbd  42257  dvbdfbdioolem2  42263  ioodvbdlimc1lem1  42265  ioodvbdlimc1lem2  42266  ioodvbdlimc2lem  42268  dvnmul  42277  dvnprodlem1  42280  dvnprodlem2  42281  iblspltprt  42307  itgspltprt  42313  stoweidlem1  42335  stoweidlem3  42337  stoweidlem5  42339  stoweidlem11  42345  stoweidlem17  42351  stoweidlem20  42354  stoweidlem26  42360  stoweidlem34  42368  wallispilem4  42402  stirlinglem11  42418  stirlinglem12  42419  stirlinglem13  42420  fourierdlem12  42453  fourierdlem15  42456  fourierdlem20  42461  fourierdlem30  42471  fourierdlem39  42480  fourierdlem42  42483  fourierdlem47  42487  fourierdlem50  42490  fourierdlem64  42504  fourierdlem65  42505  fourierdlem68  42508  fourierdlem73  42513  fourierdlem77  42517  fourierdlem79  42519  fourierdlem87  42527  elaa2lem  42567  etransclem23  42591  ioorrnopnlem  42638  salgencntex  42675  sge0le  42738  sge0isum  42758  sge0xaddlem1  42764  hoicvr  42879  hsphoidmvle2  42916  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  hoidmvlelem1  42926  hoidmvlelem2  42927  hoidmvlelem4  42929  hspmbllem1  42957  hspmbllem2  42958  smfmullem1  43115  smfmullem2  43116  smfmullem3  43117  smfsuplem1  43134  lighneallem4a  43822  fllog2  44677