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  39385  irrapxlem3  39441  irrapxlem4  39442  irrapxlem5  39443  pellexlem2  39447  pell1qrge1  39487  monotoddzzfi  39559  jm2.17a  39577  rmygeid  39581  fzmaxdif  39598  jm2.27c  39624  jm3.1lem1  39634  expdiophlem1  39638  imo72b2lem0  40536  int-ineqtransd  40567  dvgrat  40664  monoords  41584  absnpncan2d  41589  absnpncan3d  41594  ssfiunibd  41596  leadd12dd  41604  rexabslelem  41712  uzublem  41724  sqrlearg  41849  fmul01  41881  fmul01lt1lem1  41885  fmul01lt1lem2  41886  climsuselem1  41908  climsuse  41909  limsupresico  42001  limsupubuzlem  42013  limsupmnfuzlem  42027  limsupre3uzlem  42036  liminfresico  42072  limsup10exlem  42073  cnrefiisplem  42130  dvdivbd  42228  dvbdfbdioolem2  42234  ioodvbdlimc1lem1  42236  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvnmul  42248  dvnprodlem1  42251  dvnprodlem2  42252  iblspltprt  42278  itgspltprt  42284  stoweidlem1  42306  stoweidlem3  42308  stoweidlem5  42310  stoweidlem11  42316  stoweidlem17  42322  stoweidlem20  42325  stoweidlem26  42331  stoweidlem34  42339  wallispilem4  42373  stirlinglem11  42389  stirlinglem12  42390  stirlinglem13  42391  fourierdlem12  42424  fourierdlem15  42427  fourierdlem20  42432  fourierdlem30  42442  fourierdlem39  42451  fourierdlem42  42454  fourierdlem47  42458  fourierdlem50  42461  fourierdlem64  42475  fourierdlem65  42476  fourierdlem68  42479  fourierdlem73  42484  fourierdlem77  42488  fourierdlem79  42490  fourierdlem87  42498  elaa2lem  42538  etransclem23  42562  ioorrnopnlem  42609  salgencntex  42646  sge0le  42709  sge0isum  42729  sge0xaddlem1  42735  hoicvr  42850  hsphoidmvle2  42887  hoidmv1lelem1  42893  hoidmv1lelem2  42894  hoidmv1lelem3  42895  hoidmvlelem1  42897  hoidmvlelem2  42898  hoidmvlelem4  42900  hspmbllem1  42928  hspmbllem2  42929  smfmullem1  43086  smfmullem2  43087  smfmullem3  43088  smfsuplem1  43105  lighneallem4a  43793  fllog2  44648