Theorem letrd 11338

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 11275	. . 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 5110  ℝcr 11074   ≤ cle 11216

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 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714  ax-resscn 11132  ax-pre-lttri 11149  ax-pre-lttrn 11150

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 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-nel 3031  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-er 8674  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11217  df-mnf 11218  df-xr 11219  df-ltxr 11220  df-le 11221

This theorem is referenced by:  lesub3d  11803  le2addd  11804  supmul1  12159  supmul  12162  nn0negleid  12501  eluzuzle  12809  iccsplit  13453  supicc  13469  fzdisj  13519  ssfzunsnext  13537  difelfzle  13609  flwordi  13781  flleceil  13822  uzsup  13832  modltm1p1mod  13895  seqf1olem1  14013  zzlesq  14178  bernneq  14201  bernneq3  14203  discr1  14211  faclbnd  14262  faclbnd4lem1  14265  facubnd  14272  seqcoll  14436  01sqrexlem7  15221  absle  15289  releabs  15295  absrdbnd  15315  rexuzre  15326  limsupgre  15454  lo1bddrp  15498  rlimclim1  15518  rlimresb  15538  rlimrege0  15552  o1add  15587  o1sub  15589  climsqz  15614  climsqz2  15615  rlimsqzlem  15622  rlimsqz  15623  rlimsqz2  15624  rlimno1  15627  isercoll  15641  caucvgrlem  15646  iseraltlem3  15657  o1fsum  15786  cvgcmp  15789  cvgcmpce  15791  climcnds  15824  expcnv  15837  cvgrat  15856  mertenslem2  15858  fprodle  15969  eftlub  16084  rpnnen2lem12  16200  bitsfzo  16412  isprm5  16684  isprm7  16685  eulerthlem2  16759  pcmpt2  16871  pcfac  16877  prmreclem3  16896  prmreclem4  16897  prmreclem5  16898  4sqlem11  16933  vdwlem1  16959  vdwlem3  16961  setsstruct2  17151  prdsxmetlem  24263  nrmmetd  24469  nm2dif  24520  nlmvscnlem2  24580  nmoco  24632  nmotri  24634  nghmcn  24640  icccmplem2  24719  reconnlem2  24723  elii1  24838  xrhmeo  24851  cnheiborlem  24860  bndth  24864  tcphcphlem1  25142  ipcnlem2  25151  cncmet  25229  trirn  25307  minveclem2  25333  minveclem4  25339  ivthlem2  25360  ovolunlem1a  25404  ovolunlem1  25405  ovolfiniun  25409  ovoliunlem1  25410  ovolicc2lem4  25428  ovolicc2lem5  25429  ovolicopnf  25432  nulmbl2  25444  ioombl1lem4  25469  ioorcl2  25480  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  volcn  25514  vitalilem2  25517  vitali  25521  mbfi1fseqlem5  25627  mbfi1fseqlem6  25628  itg2splitlem  25656  itg2monolem1  25658  itg2monolem3  25660  itg2mono  25661  itg2cnlem1  25669  itgle  25718  bddmulibl  25747  bddiblnc  25750  ditgsplitlem  25768  dveflem  25890  dvlip  25905  dveq0  25912  dvfsumabs  25936  dvfsumlem1  25939  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  dvfsumlem4  25943  dvfsum2  25948  fta1glem2  26081  dgradd2  26181  plydiveu  26213  fta1lem  26222  aalioulem2  26248  aalioulem3  26249  aalioulem4  26250  aalioulem5  26251  aaliou3lem8  26260  aaliou3lem9  26265  ulmbdd  26314  ulmcn  26315  mtest  26320  mtestbdd  26321  abelthlem2  26349  abelthlem7  26355  pilem2  26369  tanabsge  26422  cosordlem  26446  tanord  26454  logneg2  26531  abslogle  26534  dvlog2lem  26568  cxple2a  26615  abscxpbnd  26670  atans2  26848  leibpi  26859  o1cxp  26892  cxploglim2  26896  jensenlem2  26905  emcllem6  26918  harmoniclbnd  26926  harmonicubnd  26927  harmonicbnd4  26928  fsumharmonic  26929  lgamgulmlem2  26947  lgamgulmlem3  26948  lgamgulmlem5  26950  lgambdd  26954  ftalem2  26991  basellem3  27000  basellem5  27002  basellem6  27003  dvdsflsumcom  27105  fsumfldivdiaglem  27106  ppiub  27122  chtublem  27129  logfac2  27135  chpub  27138  logfacubnd  27139  logfaclbnd  27140  logfacbnd3  27141  logexprlim  27143  bcmono  27195  bpos1lem  27200  bposlem1  27202  bposlem2  27203  bposlem3  27204  bposlem4  27205  bposlem5  27206  bposlem6  27207  bposlem7  27208  bposlem9  27210  lgsdirprm  27249  lgsquadlem1  27298  2lgslem1c  27311  2sqlem8  27344  chebbnd1lem1  27387  chebbnd1lem3  27389  chtppilimlem1  27391  chpchtlim  27397  vmadivsumb  27401  rplogsumlem1  27402  rplogsumlem2  27403  rpvmasumlem  27405  dchrisumlema  27406  dchrisumlem2  27408  dchrisumlem3  27409  dchrmusum2  27412  dchrvmasumlem2  27416  dchrvmasumlem3  27417  dchrvmasumlema  27418  dchrvmasumiflem1  27419  dchrisum0flblem1  27426  dchrisum0flblem2  27427  dchrisum0fno1  27429  dchrisum0re  27431  dchrisum0lem1b  27433  dchrisum0lem1  27434  dchrisum0lem2a  27435  dchrisum0  27438  rplogsum  27445  mudivsum  27448  mulogsumlem  27449  logdivsum  27451  mulog2sumlem1  27452  mulog2sumlem2  27453  2vmadivsumlem  27458  log2sumbnd  27462  selberglem2  27464  selbergb  27467  selberg2lem  27468  selberg2b  27470  chpdifbndlem1  27471  logdivbnd  27474  selberg3lem1  27475  selberg3lem2  27476  selberg4lem1  27478  pntrmax  27482  pntrsumo1  27483  pntrsumbnd  27484  pntrlog2bndlem1  27495  pntrlog2bndlem2  27496  pntrlog2bndlem3  27497  pntrlog2bndlem5  27499  pntrlog2bndlem6  27501  pntrlog2bnd  27502  pntpbnd1a  27503  pntpbnd1  27504  pntpbnd2  27505  pntibndlem2  27509  pntibndlem3  27510  pntlemg  27516  pntlemr  27520  pntlemj  27521  pntlemf  27523  pntlemk  27524  pntlemo  27525  pntleml  27529  abvcxp  27533  qabvle  27543  padicabv  27548  ostth2lem2  27552  ostth2lem3  27553  ostth3  27556  axlowdimlem16  28891  axcontlem8  28905  axcontlem10  28907  wwlksm1edg  29818  wwlksubclwwlk  29994  smcnlem  30633  nmoub3i  30709  ubthlem3  30808  minvecolem2  30811  minvecolem3  30812  minvecolem4  30816  htthlem  30853  bcs2  31118  pjhthlem1  31327  cnlnadjlem2  32004  cnlnadjlem7  32009  nmopadjlem  32025  nmoptrii  32030  nmopcoadji  32037  leopnmid  32074  cdj1i  32369  nndiffz1  32716  nexple  32776  oexpled  32779  pmtrto1cl  33063  psgnfzto1stlem  33064  fzto1st  33067  psgnfzto1st  33069  cyc3conja  33121  constrresqrtcl  33774  cos9thpiminplylem1  33779  smatrcl  33793  submateqlem1  33804  esumpcvgval  34075  oddpwdc  34352  eulerpartlems  34358  eulerpartlemgc  34360  eulerpartlemb  34366  dstfrvunirn  34473  orvclteinc  34474  ballotlemsima  34514  ballotlemfrcn0  34528  signstfveq0  34575  fsum2dsub  34605  breprexplemc  34630  breprexp  34631  logdivsqrle  34648  hgt750lemb  34654  hgt750leme  34656  tgoldbachgnn  34657  dnibndlem2  36474  dnibndlem6  36478  dnibndlem9  36481  dnibndlem10  36482  dnibndlem11  36483  dnibndlem12  36484  knoppcnlem4  36491  unblimceq0lem  36501  unblimceq0  36502  unbdqndv2lem2  36505  knoppndvlem11  36517  knoppndvlem14  36520  knoppndvlem15  36521  knoppndvlem18  36524  knoppndvlem21  36527  poimirlem6  37627  poimirlem7  37628  poimirlem13  37634  poimirlem15  37636  poimirlem29  37650  mblfinlem2  37659  mblfinlem3  37660  mblfinlem4  37661  ismblfin  37662  itg2addnc  37675  iblmulc2nc  37686  ftc1anclem7  37700  ftc1anclem8  37701  filbcmb  37741  geomcau  37760  prdsbnd  37794  cntotbnd  37797  bfplem2  37824  rrntotbnd  37837  iccbnd  37841  lcmineqlem20  42043  lcmineqlem21  42044  lcmineqlem22  42045  3lexlogpow5ineq2  42050  3lexlogpow5ineq5  42055  aks4d1p1p2  42065  aks4d1p1p4  42066  aks4d1p1p7  42069  aks4d1p1p5  42070  aks4d1p1  42071  aks4d1p2  42072  aks4d1p3  42073  aks4d1p5  42075  aks4d1p6  42076  aks4d1p7d1  42077  aks4d1p7  42078  aks4d1p8  42082  posbezout  42095  aks6d1c1  42111  aks6d1c2lem4  42122  2np3bcnp1  42139  sticksstones6  42146  sticksstones7  42147  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  sticksstones22  42163  bcled  42173  bcle2d  42174  aks6d1c7lem1  42175  aks6d1c7lem2  42176  unitscyglem4  42193  lzunuz  42763  irrapxlem3  42819  irrapxlem4  42820  irrapxlem5  42821  pellexlem2  42825  pell1qrge1  42865  monotoddzzfi  42938  jm2.17a  42956  rmygeid  42960  fzmaxdif  42977  jm2.27c  43003  jm3.1lem1  43013  expdiophlem1  43017  fzunt  43451  fzuntd  43452  fzunt1d  43453  fzuntgd  43454  imo72b2lem0  44161  int-ineqtransd  44190  dvgrat  44308  monoords  45302  absnpncan2d  45307  absnpncan3d  45312  ssfiunibd  45314  rexabslelem  45421  uzublem  45433  sqrlearg  45558  fmul01  45585  fmul01lt1lem1  45589  fmul01lt1lem2  45590  climsuselem1  45612  climsuse  45613  limsupresico  45705  limsupubuzlem  45717  limsupmnfuzlem  45731  limsupre3uzlem  45740  liminfresico  45776  limsup10exlem  45777  cnrefiisplem  45834  dvdivbd  45928  dvbdfbdioolem2  45934  ioodvbdlimc1lem1  45936  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnmul  45948  dvnprodlem1  45951  dvnprodlem2  45952  iblspltprt  45978  itgspltprt  45984  stoweidlem1  46006  stoweidlem3  46008  stoweidlem5  46010  stoweidlem11  46016  stoweidlem17  46022  stoweidlem20  46025  stoweidlem26  46031  stoweidlem34  46039  wallispilem4  46073  stirlinglem11  46089  stirlinglem12  46090  stirlinglem13  46091  fourierdlem12  46124  fourierdlem15  46127  fourierdlem20  46132  fourierdlem30  46142  fourierdlem39  46151  fourierdlem42  46154  fourierdlem47  46158  fourierdlem50  46161  fourierdlem64  46175  fourierdlem65  46176  fourierdlem68  46179  fourierdlem73  46184  fourierdlem77  46188  fourierdlem79  46190  fourierdlem87  46198  elaa2lem  46238  etransclem23  46262  ioorrnopnlem  46309  salgencntex  46348  sge0le  46412  sge0isum  46432  sge0xaddlem1  46438  hoicvr  46553  hsphoidmvle2  46590  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1lelem3  46598  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem4  46603  hspmbllem1  46631  hspmbllem2  46632  smfmullem1  46796  smfmullem2  46797  smfmullem3  46798  smfsuplem1  46816  ormkglobd  46880  natglobalincr  46882  2ltceilhalf  47333  ceilhalfnn  47341  modmknepk  47367  lighneallem4a  47613  gpgusgralem  48051  gpgedgvtx1  48057  gpg3kgrtriexlem4  48081  gpg3kgrtriexlem6  48083  fllog2  48561  itcovalt2lem2lem1  48666