Theorem letrd 11331

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5107  ℝcr 11067   ≤ cle 11209

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-resscn 11125  ax-pre-lttri 11142  ax-pre-lttrn 11143

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 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214

This theorem is referenced by:  lesub3d  11796  le2addd  11797  supmul1  12152  supmul  12155  nn0negleid  12494  eluzuzle  12802  iccsplit  13446  supicc  13462  fzdisj  13512  ssfzunsnext  13530  difelfzle  13602  flwordi  13774  flleceil  13815  uzsup  13825  modltm1p1mod  13888  seqf1olem1  14006  zzlesq  14171  bernneq  14194  bernneq3  14196  discr1  14204  faclbnd  14255  faclbnd4lem1  14258  facubnd  14265  seqcoll  14429  01sqrexlem7  15214  absle  15282  releabs  15288  absrdbnd  15308  rexuzre  15319  limsupgre  15447  lo1bddrp  15491  rlimclim1  15511  rlimresb  15531  rlimrege0  15545  o1add  15580  o1sub  15582  climsqz  15607  climsqz2  15608  rlimsqzlem  15615  rlimsqz  15616  rlimsqz2  15617  rlimno1  15620  isercoll  15634  caucvgrlem  15639  iseraltlem3  15650  o1fsum  15779  cvgcmp  15782  cvgcmpce  15784  climcnds  15817  expcnv  15830  cvgrat  15849  mertenslem2  15851  fprodle  15962  eftlub  16077  rpnnen2lem12  16193  bitsfzo  16405  isprm5  16677  isprm7  16678  eulerthlem2  16752  pcmpt2  16864  pcfac  16870  prmreclem3  16889  prmreclem4  16890  prmreclem5  16891  4sqlem11  16926  vdwlem1  16952  vdwlem3  16954  setsstruct2  17144  prdsxmetlem  24256  nrmmetd  24462  nm2dif  24513  nlmvscnlem2  24573  nmoco  24625  nmotri  24627  nghmcn  24633  icccmplem2  24712  reconnlem2  24716  elii1  24831  xrhmeo  24844  cnheiborlem  24853  bndth  24857  tcphcphlem1  25135  ipcnlem2  25144  cncmet  25222  trirn  25300  minveclem2  25326  minveclem4  25332  ivthlem2  25353  ovolunlem1a  25397  ovolunlem1  25398  ovolfiniun  25402  ovoliunlem1  25403  ovolicc2lem4  25421  ovolicc2lem5  25422  ovolicopnf  25425  nulmbl2  25437  ioombl1lem4  25462  ioorcl2  25473  uniioombllem3  25486  uniioombllem4  25487  uniioombllem5  25488  volcn  25507  vitalilem2  25510  vitali  25514  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  itg2splitlem  25649  itg2monolem1  25651  itg2monolem3  25653  itg2mono  25654  itg2cnlem1  25662  itgle  25711  bddmulibl  25740  bddiblnc  25743  ditgsplitlem  25761  dveflem  25883  dvlip  25898  dveq0  25905  dvfsumabs  25929  dvfsumlem1  25932  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumlem3  25935  dvfsumlem4  25936  dvfsum2  25941  fta1glem2  26074  dgradd2  26174  plydiveu  26206  fta1lem  26215  aalioulem2  26241  aalioulem3  26242  aalioulem4  26243  aalioulem5  26244  aaliou3lem8  26253  aaliou3lem9  26258  ulmbdd  26307  ulmcn  26308  mtest  26313  mtestbdd  26314  abelthlem2  26342  abelthlem7  26348  pilem2  26362  tanabsge  26415  cosordlem  26439  tanord  26447  logneg2  26524  abslogle  26527  dvlog2lem  26561  cxple2a  26608  abscxpbnd  26663  atans2  26841  leibpi  26852  o1cxp  26885  cxploglim2  26889  jensenlem2  26898  emcllem6  26911  harmoniclbnd  26919  harmonicubnd  26920  harmonicbnd4  26921  fsumharmonic  26922  lgamgulmlem2  26940  lgamgulmlem3  26941  lgamgulmlem5  26943  lgambdd  26947  ftalem2  26984  basellem3  26993  basellem5  26995  basellem6  26996  dvdsflsumcom  27098  fsumfldivdiaglem  27099  ppiub  27115  chtublem  27122  logfac2  27128  chpub  27131  logfacubnd  27132  logfaclbnd  27133  logfacbnd3  27134  logexprlim  27136  bcmono  27188  bpos1lem  27193  bposlem1  27195  bposlem2  27196  bposlem3  27197  bposlem4  27198  bposlem5  27199  bposlem6  27200  bposlem7  27201  bposlem9  27203  lgsdirprm  27242  lgsquadlem1  27291  2lgslem1c  27304  2sqlem8  27337  chebbnd1lem1  27380  chebbnd1lem3  27382  chtppilimlem1  27384  chpchtlim  27390  vmadivsumb  27394  rplogsumlem1  27395  rplogsumlem2  27396  rpvmasumlem  27398  dchrisumlema  27399  dchrisumlem2  27401  dchrisumlem3  27402  dchrmusum2  27405  dchrvmasumlem2  27409  dchrvmasumlem3  27410  dchrvmasumlema  27411  dchrvmasumiflem1  27412  dchrisum0flblem1  27419  dchrisum0flblem2  27420  dchrisum0fno1  27422  dchrisum0re  27424  dchrisum0lem1b  27426  dchrisum0lem1  27427  dchrisum0lem2a  27428  dchrisum0  27431  rplogsum  27438  mudivsum  27441  mulogsumlem  27442  logdivsum  27444  mulog2sumlem1  27445  mulog2sumlem2  27446  2vmadivsumlem  27451  log2sumbnd  27455  selberglem2  27457  selbergb  27460  selberg2lem  27461  selberg2b  27463  chpdifbndlem1  27464  logdivbnd  27467  selberg3lem1  27468  selberg3lem2  27469  selberg4lem1  27471  pntrmax  27475  pntrsumo1  27476  pntrsumbnd  27477  pntrlog2bndlem1  27488  pntrlog2bndlem2  27489  pntrlog2bndlem3  27490  pntrlog2bndlem5  27492  pntrlog2bndlem6  27494  pntrlog2bnd  27495  pntpbnd1a  27496  pntpbnd1  27497  pntpbnd2  27498  pntibndlem2  27502  pntibndlem3  27503  pntlemg  27509  pntlemr  27513  pntlemj  27514  pntlemf  27516  pntlemk  27517  pntlemo  27518  pntleml  27522  abvcxp  27526  qabvle  27536  padicabv  27541  ostth2lem2  27545  ostth2lem3  27546  ostth3  27549  axlowdimlem16  28884  axcontlem8  28898  axcontlem10  28900  wwlksm1edg  29811  wwlksubclwwlk  29987  smcnlem  30626  nmoub3i  30702  ubthlem3  30801  minvecolem2  30804  minvecolem3  30805  minvecolem4  30809  htthlem  30846  bcs2  31111  pjhthlem1  31320  cnlnadjlem2  31997  cnlnadjlem7  32002  nmopadjlem  32018  nmoptrii  32023  nmopcoadji  32030  leopnmid  32067  cdj1i  32362  nndiffz1  32709  nexple  32769  oexpled  32772  pmtrto1cl  33056  psgnfzto1stlem  33057  fzto1st  33060  psgnfzto1st  33062  cyc3conja  33114  constrresqrtcl  33767  cos9thpiminplylem1  33772  smatrcl  33786  submateqlem1  33797  esumpcvgval  34068  oddpwdc  34345  eulerpartlems  34351  eulerpartlemgc  34353  eulerpartlemb  34359  dstfrvunirn  34466  orvclteinc  34467  ballotlemsima  34507  ballotlemfrcn0  34521  signstfveq0  34568  fsum2dsub  34598  breprexplemc  34623  breprexp  34624  logdivsqrle  34641  hgt750lemb  34647  hgt750leme  34649  tgoldbachgnn  34650  dnibndlem2  36467  dnibndlem6  36471  dnibndlem9  36474  dnibndlem10  36475  dnibndlem11  36476  dnibndlem12  36477  knoppcnlem4  36484  unblimceq0lem  36494  unblimceq0  36495  unbdqndv2lem2  36498  knoppndvlem11  36510  knoppndvlem14  36513  knoppndvlem15  36514  knoppndvlem18  36517  knoppndvlem21  36520  poimirlem6  37620  poimirlem7  37621  poimirlem13  37627  poimirlem15  37629  poimirlem29  37643  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  itg2addnc  37668  iblmulc2nc  37679  ftc1anclem7  37693  ftc1anclem8  37694  filbcmb  37734  geomcau  37753  prdsbnd  37787  cntotbnd  37790  bfplem2  37817  rrntotbnd  37830  iccbnd  37834  lcmineqlem20  42036  lcmineqlem21  42037  lcmineqlem22  42038  3lexlogpow5ineq2  42043  3lexlogpow5ineq5  42048  aks4d1p1p2  42058  aks4d1p1p4  42059  aks4d1p1p7  42062  aks4d1p1p5  42063  aks4d1p1  42064  aks4d1p2  42065  aks4d1p3  42066  aks4d1p5  42068  aks4d1p6  42069  aks4d1p7d1  42070  aks4d1p7  42071  aks4d1p8  42075  posbezout  42088  aks6d1c1  42104  aks6d1c2lem4  42115  2np3bcnp1  42132  sticksstones6  42139  sticksstones7  42140  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones22  42156  bcled  42166  bcle2d  42167  aks6d1c7lem1  42168  aks6d1c7lem2  42169  unitscyglem4  42186  lzunuz  42756  irrapxlem3  42812  irrapxlem4  42813  irrapxlem5  42814  pellexlem2  42818  pell1qrge1  42858  monotoddzzfi  42931  jm2.17a  42949  rmygeid  42953  fzmaxdif  42970  jm2.27c  42996  jm3.1lem1  43006  expdiophlem1  43010  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  imo72b2lem0  44154  int-ineqtransd  44183  dvgrat  44301  monoords  45295  absnpncan2d  45300  absnpncan3d  45305  ssfiunibd  45307  rexabslelem  45414  uzublem  45426  sqrlearg  45551  fmul01  45578  fmul01lt1lem1  45582  fmul01lt1lem2  45583  climsuselem1  45605  climsuse  45606  limsupresico  45698  limsupubuzlem  45710  limsupmnfuzlem  45724  limsupre3uzlem  45733  liminfresico  45769  limsup10exlem  45770  cnrefiisplem  45827  dvdivbd  45921  dvbdfbdioolem2  45927  ioodvbdlimc1lem1  45929  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnmul  45941  dvnprodlem1  45944  dvnprodlem2  45945  iblspltprt  45971  itgspltprt  45977  stoweidlem1  45999  stoweidlem3  46001  stoweidlem5  46003  stoweidlem11  46009  stoweidlem17  46015  stoweidlem20  46018  stoweidlem26  46024  stoweidlem34  46032  wallispilem4  46066  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  fourierdlem12  46117  fourierdlem15  46120  fourierdlem20  46125  fourierdlem30  46135  fourierdlem39  46144  fourierdlem42  46147  fourierdlem47  46151  fourierdlem50  46154  fourierdlem64  46168  fourierdlem65  46169  fourierdlem68  46172  fourierdlem73  46177  fourierdlem77  46181  fourierdlem79  46183  fourierdlem87  46191  elaa2lem  46231  etransclem23  46255  ioorrnopnlem  46302  salgencntex  46341  sge0le  46405  sge0isum  46425  sge0xaddlem1  46431  hoicvr  46546  hsphoidmvle2  46583  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem4  46596  hspmbllem1  46624  hspmbllem2  46625  smfmullem1  46789  smfmullem2  46790  smfmullem3  46791  smfsuplem1  46809  ormkglobd  46873  natglobalincr  46875  2ltceilhalf  47329  ceilhalfnn  47337  modmknepk  47363  lighneallem4a  47609  gpgusgralem  48047  gpgedgvtx1  48053  gpg3kgrtriexlem4  48077  gpg3kgrtriexlem6  48079  fllog2  48557  itcovalt2lem2lem1  48662