Theorem letrd 11261

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 11198	. . 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 5088  ℝcr 10996   ≤ cle 11138

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 5231  ax-nul 5241  ax-pow 5300  ax-pr 5367  ax-un 7662  ax-resscn 11054  ax-pre-lttri 11071  ax-pre-lttrn 11072

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 3393  df-v 3435  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5089  df-opab 5151  df-mpt 5170  df-id 5508  df-xp 5619  df-rel 5620  df-cnv 5621  df-co 5622  df-dm 5623  df-rn 5624  df-res 5625  df-ima 5626  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483  df-fv 6484  df-er 8616  df-en 8864  df-dom 8865  df-sdom 8866  df-pnf 11139  df-mnf 11140  df-xr 11141  df-ltxr 11142  df-le 11143

This theorem is referenced by:  lesub3d  11726  le2addd  11727  supmul1  12082  supmul  12085  nn0negleid  12424  eluzuzle  12732  iccsplit  13376  supicc  13392  fzdisj  13442  ssfzunsnext  13460  difelfzle  13532  flwordi  13704  flleceil  13745  uzsup  13755  modltm1p1mod  13818  seqf1olem1  13936  zzlesq  14101  bernneq  14124  bernneq3  14126  discr1  14134  faclbnd  14185  faclbnd4lem1  14188  facubnd  14195  seqcoll  14359  01sqrexlem7  15142  absle  15210  releabs  15216  absrdbnd  15236  rexuzre  15247  limsupgre  15375  lo1bddrp  15419  rlimclim1  15439  rlimresb  15459  rlimrege0  15473  o1add  15508  o1sub  15510  climsqz  15535  climsqz2  15536  rlimsqzlem  15543  rlimsqz  15544  rlimsqz2  15545  rlimno1  15548  isercoll  15562  caucvgrlem  15567  iseraltlem3  15578  o1fsum  15707  cvgcmp  15710  cvgcmpce  15712  climcnds  15745  expcnv  15758  cvgrat  15777  mertenslem2  15779  fprodle  15890  eftlub  16005  rpnnen2lem12  16121  bitsfzo  16333  isprm5  16605  isprm7  16606  eulerthlem2  16680  pcmpt2  16792  pcfac  16798  prmreclem3  16817  prmreclem4  16818  prmreclem5  16819  4sqlem11  16854  vdwlem1  16880  vdwlem3  16882  setsstruct2  17072  prdsxmetlem  24237  nrmmetd  24443  nm2dif  24494  nlmvscnlem2  24554  nmoco  24606  nmotri  24608  nghmcn  24614  icccmplem2  24693  reconnlem2  24697  elii1  24812  xrhmeo  24825  cnheiborlem  24834  bndth  24838  tcphcphlem1  25116  ipcnlem2  25125  cncmet  25203  trirn  25281  minveclem2  25307  minveclem4  25313  ivthlem2  25334  ovolunlem1a  25378  ovolunlem1  25379  ovolfiniun  25383  ovoliunlem1  25384  ovolicc2lem4  25402  ovolicc2lem5  25403  ovolicopnf  25406  nulmbl2  25418  ioombl1lem4  25443  ioorcl2  25454  uniioombllem3  25467  uniioombllem4  25468  uniioombllem5  25469  volcn  25488  vitalilem2  25491  vitali  25495  mbfi1fseqlem5  25601  mbfi1fseqlem6  25602  itg2splitlem  25630  itg2monolem1  25632  itg2monolem3  25634  itg2mono  25635  itg2cnlem1  25643  itgle  25692  bddmulibl  25721  bddiblnc  25724  ditgsplitlem  25742  dveflem  25864  dvlip  25879  dveq0  25886  dvfsumabs  25910  dvfsumlem1  25913  dvfsumlem2  25914  dvfsumlem2OLD  25915  dvfsumlem3  25916  dvfsumlem4  25917  dvfsum2  25922  fta1glem2  26055  dgradd2  26155  plydiveu  26187  fta1lem  26196  aalioulem2  26222  aalioulem3  26223  aalioulem4  26224  aalioulem5  26225  aaliou3lem8  26234  aaliou3lem9  26239  ulmbdd  26288  ulmcn  26289  mtest  26294  mtestbdd  26295  abelthlem2  26323  abelthlem7  26329  pilem2  26343  tanabsge  26396  cosordlem  26420  tanord  26428  logneg2  26505  abslogle  26508  dvlog2lem  26542  cxple2a  26589  abscxpbnd  26644  atans2  26822  leibpi  26833  o1cxp  26866  cxploglim2  26870  jensenlem2  26879  emcllem6  26892  harmoniclbnd  26900  harmonicubnd  26901  harmonicbnd4  26902  fsumharmonic  26903  lgamgulmlem2  26921  lgamgulmlem3  26922  lgamgulmlem5  26924  lgambdd  26928  ftalem2  26965  basellem3  26974  basellem5  26976  basellem6  26977  dvdsflsumcom  27079  fsumfldivdiaglem  27080  ppiub  27096  chtublem  27103  logfac2  27109  chpub  27112  logfacubnd  27113  logfaclbnd  27114  logfacbnd3  27115  logexprlim  27117  bcmono  27169  bpos1lem  27174  bposlem1  27176  bposlem2  27177  bposlem3  27178  bposlem4  27179  bposlem5  27180  bposlem6  27181  bposlem7  27182  bposlem9  27184  lgsdirprm  27223  lgsquadlem1  27272  2lgslem1c  27285  2sqlem8  27318  chebbnd1lem1  27361  chebbnd1lem3  27363  chtppilimlem1  27365  chpchtlim  27371  vmadivsumb  27375  rplogsumlem1  27376  rplogsumlem2  27377  rpvmasumlem  27379  dchrisumlema  27380  dchrisumlem2  27382  dchrisumlem3  27383  dchrmusum2  27386  dchrvmasumlem2  27390  dchrvmasumlem3  27391  dchrvmasumlema  27392  dchrvmasumiflem1  27393  dchrisum0flblem1  27400  dchrisum0flblem2  27401  dchrisum0fno1  27403  dchrisum0re  27405  dchrisum0lem1b  27407  dchrisum0lem1  27408  dchrisum0lem2a  27409  dchrisum0  27412  rplogsum  27419  mudivsum  27422  mulogsumlem  27423  logdivsum  27425  mulog2sumlem1  27426  mulog2sumlem2  27427  2vmadivsumlem  27432  log2sumbnd  27436  selberglem2  27438  selbergb  27441  selberg2lem  27442  selberg2b  27444  chpdifbndlem1  27445  logdivbnd  27448  selberg3lem1  27449  selberg3lem2  27450  selberg4lem1  27452  pntrmax  27456  pntrsumo1  27457  pntrsumbnd  27458  pntrlog2bndlem1  27469  pntrlog2bndlem2  27470  pntrlog2bndlem3  27471  pntrlog2bndlem5  27473  pntrlog2bndlem6  27475  pntrlog2bnd  27476  pntpbnd1a  27477  pntpbnd1  27478  pntpbnd2  27479  pntibndlem2  27483  pntibndlem3  27484  pntlemg  27490  pntlemr  27494  pntlemj  27495  pntlemf  27497  pntlemk  27498  pntlemo  27499  pntleml  27503  abvcxp  27507  qabvle  27517  padicabv  27522  ostth2lem2  27526  ostth2lem3  27527  ostth3  27530  axlowdimlem16  28889  axcontlem8  28903  axcontlem10  28905  wwlksm1edg  29813  wwlksubclwwlk  29989  smcnlem  30628  nmoub3i  30704  ubthlem3  30803  minvecolem2  30806  minvecolem3  30807  minvecolem4  30811  htthlem  30848  bcs2  31113  pjhthlem1  31322  cnlnadjlem2  31999  cnlnadjlem7  32004  nmopadjlem  32020  nmoptrii  32025  nmopcoadji  32032  leopnmid  32069  cdj1i  32364  nndiffz1  32721  nexple  32782  oexpled  32785  pmtrto1cl  33036  psgnfzto1stlem  33037  fzto1st  33040  psgnfzto1st  33042  cyc3conja  33094  constrresqrtcl  33758  cos9thpiminplylem1  33763  smatrcl  33777  submateqlem1  33788  esumpcvgval  34059  oddpwdc  34335  eulerpartlems  34341  eulerpartlemgc  34343  eulerpartlemb  34349  dstfrvunirn  34456  orvclteinc  34457  ballotlemsima  34497  ballotlemfrcn0  34511  signstfveq0  34558  fsum2dsub  34588  breprexplemc  34613  breprexp  34614  logdivsqrle  34631  hgt750lemb  34637  hgt750leme  34639  tgoldbachgnn  34640  dnibndlem2  36470  dnibndlem6  36474  dnibndlem9  36477  dnibndlem10  36478  dnibndlem11  36479  dnibndlem12  36480  knoppcnlem4  36487  unblimceq0lem  36497  unblimceq0  36498  unbdqndv2lem2  36501  knoppndvlem11  36513  knoppndvlem14  36516  knoppndvlem15  36517  knoppndvlem18  36520  knoppndvlem21  36523  poimirlem6  37623  poimirlem7  37624  poimirlem13  37630  poimirlem15  37632  poimirlem29  37646  mblfinlem2  37655  mblfinlem3  37656  mblfinlem4  37657  ismblfin  37658  itg2addnc  37671  iblmulc2nc  37682  ftc1anclem7  37696  ftc1anclem8  37697  filbcmb  37737  geomcau  37756  prdsbnd  37790  cntotbnd  37793  bfplem2  37820  rrntotbnd  37833  iccbnd  37837  lcmineqlem20  42038  lcmineqlem21  42039  lcmineqlem22  42040  3lexlogpow5ineq2  42045  3lexlogpow5ineq5  42050  aks4d1p1p2  42060  aks4d1p1p4  42061  aks4d1p1p7  42064  aks4d1p1p5  42065  aks4d1p1  42066  aks4d1p2  42067  aks4d1p3  42068  aks4d1p5  42070  aks4d1p6  42071  aks4d1p7d1  42072  aks4d1p7  42073  aks4d1p8  42077  posbezout  42090  aks6d1c1  42106  aks6d1c2lem4  42117  2np3bcnp1  42134  sticksstones6  42141  sticksstones7  42142  sticksstones10  42145  sticksstones12a  42147  sticksstones12  42148  sticksstones22  42158  bcled  42168  bcle2d  42169  aks6d1c7lem1  42170  aks6d1c7lem2  42171  unitscyglem4  42188  lzunuz  42758  irrapxlem3  42814  irrapxlem4  42815  irrapxlem5  42816  pellexlem2  42820  pell1qrge1  42860  monotoddzzfi  42932  jm2.17a  42950  rmygeid  42954  fzmaxdif  42971  jm2.27c  42997  jm3.1lem1  43007  expdiophlem1  43011  fzunt  43445  fzuntd  43446  fzunt1d  43447  fzuntgd  43448  imo72b2lem0  44155  int-ineqtransd  44184  dvgrat  44302  monoords  45295  absnpncan2d  45300  absnpncan3d  45305  ssfiunibd  45307  rexabslelem  45413  uzublem  45425  sqrlearg  45550  fmul01  45577  fmul01lt1lem1  45581  fmul01lt1lem2  45582  climsuselem1  45604  climsuse  45605  limsupresico  45695  limsupubuzlem  45707  limsupmnfuzlem  45721  limsupre3uzlem  45730  liminfresico  45766  limsup10exlem  45767  cnrefiisplem  45824  dvdivbd  45918  dvbdfbdioolem2  45924  ioodvbdlimc1lem1  45926  ioodvbdlimc1lem2  45927  ioodvbdlimc2lem  45929  dvnmul  45938  dvnprodlem1  45941  dvnprodlem2  45942  iblspltprt  45968  itgspltprt  45974  stoweidlem1  45996  stoweidlem3  45998  stoweidlem5  46000  stoweidlem11  46006  stoweidlem17  46012  stoweidlem20  46015  stoweidlem26  46021  stoweidlem34  46029  wallispilem4  46063  stirlinglem11  46079  stirlinglem12  46080  stirlinglem13  46081  fourierdlem12  46114  fourierdlem15  46117  fourierdlem20  46122  fourierdlem30  46132  fourierdlem39  46141  fourierdlem42  46144  fourierdlem47  46148  fourierdlem50  46151  fourierdlem64  46165  fourierdlem65  46166  fourierdlem68  46169  fourierdlem73  46174  fourierdlem77  46178  fourierdlem79  46180  fourierdlem87  46188  elaa2lem  46228  etransclem23  46252  ioorrnopnlem  46299  salgencntex  46338  sge0le  46402  sge0isum  46422  sge0xaddlem1  46428  hoicvr  46543  hsphoidmvle2  46580  hoidmv1lelem1  46586  hoidmv1lelem2  46587  hoidmv1lelem3  46588  hoidmvlelem1  46590  hoidmvlelem2  46591  hoidmvlelem4  46593  hspmbllem1  46621  hspmbllem2  46622  smfmullem1  46786  smfmullem2  46787  smfmullem3  46788  smfsuplem1  46806  ormkglobd  46870  natglobalincr  46872  2ltceilhalf  47326  ceilhalfnn  47334  modmknepk  47360  lighneallem4a  47606  gpgusgralem  48054  gpgedgvtx1  48060  gpg3kgrtriexlem4  48084  gpg3kgrtriexlem6  48086  fllog2  48567  itcovalt2lem2lem1  48672