Theorem letrd 11307

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 11244	. . 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 5102  ℝcr 11043   ≤ cle 11185

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 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-pre-lttri 11118  ax-pre-lttrn 11119

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 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190

This theorem is referenced by:  lesub3d  11772  le2addd  11773  supmul1  12128  supmul  12131  nn0negleid  12470  eluzuzle  12778  iccsplit  13422  supicc  13438  fzdisj  13488  ssfzunsnext  13506  difelfzle  13578  flwordi  13750  flleceil  13791  uzsup  13801  modltm1p1mod  13864  seqf1olem1  13982  zzlesq  14147  bernneq  14170  bernneq3  14172  discr1  14180  faclbnd  14231  faclbnd4lem1  14234  facubnd  14241  seqcoll  14405  01sqrexlem7  15190  absle  15258  releabs  15264  absrdbnd  15284  rexuzre  15295  limsupgre  15423  lo1bddrp  15467  rlimclim1  15487  rlimresb  15507  rlimrege0  15521  o1add  15556  o1sub  15558  climsqz  15583  climsqz2  15584  rlimsqzlem  15591  rlimsqz  15592  rlimsqz2  15593  rlimno1  15596  isercoll  15610  caucvgrlem  15615  iseraltlem3  15626  o1fsum  15755  cvgcmp  15758  cvgcmpce  15760  climcnds  15793  expcnv  15806  cvgrat  15825  mertenslem2  15827  fprodle  15938  eftlub  16053  rpnnen2lem12  16169  bitsfzo  16381  isprm5  16653  isprm7  16654  eulerthlem2  16728  pcmpt2  16840  pcfac  16846  prmreclem3  16865  prmreclem4  16866  prmreclem5  16867  4sqlem11  16902  vdwlem1  16928  vdwlem3  16930  setsstruct2  17120  prdsxmetlem  24232  nrmmetd  24438  nm2dif  24489  nlmvscnlem2  24549  nmoco  24601  nmotri  24603  nghmcn  24609  icccmplem2  24688  reconnlem2  24692  elii1  24807  xrhmeo  24820  cnheiborlem  24829  bndth  24833  tcphcphlem1  25111  ipcnlem2  25120  cncmet  25198  trirn  25276  minveclem2  25302  minveclem4  25308  ivthlem2  25329  ovolunlem1a  25373  ovolunlem1  25374  ovolfiniun  25378  ovoliunlem1  25379  ovolicc2lem4  25397  ovolicc2lem5  25398  ovolicopnf  25401  nulmbl2  25413  ioombl1lem4  25438  ioorcl2  25449  uniioombllem3  25462  uniioombllem4  25463  uniioombllem5  25464  volcn  25483  vitalilem2  25486  vitali  25490  mbfi1fseqlem5  25596  mbfi1fseqlem6  25597  itg2splitlem  25625  itg2monolem1  25627  itg2monolem3  25629  itg2mono  25630  itg2cnlem1  25638  itgle  25687  bddmulibl  25716  bddiblnc  25719  ditgsplitlem  25737  dveflem  25859  dvlip  25874  dveq0  25881  dvfsumabs  25905  dvfsumlem1  25908  dvfsumlem2  25909  dvfsumlem2OLD  25910  dvfsumlem3  25911  dvfsumlem4  25912  dvfsum2  25917  fta1glem2  26050  dgradd2  26150  plydiveu  26182  fta1lem  26191  aalioulem2  26217  aalioulem3  26218  aalioulem4  26219  aalioulem5  26220  aaliou3lem8  26229  aaliou3lem9  26234  ulmbdd  26283  ulmcn  26284  mtest  26289  mtestbdd  26290  abelthlem2  26318  abelthlem7  26324  pilem2  26338  tanabsge  26391  cosordlem  26415  tanord  26423  logneg2  26500  abslogle  26503  dvlog2lem  26537  cxple2a  26584  abscxpbnd  26639  atans2  26817  leibpi  26828  o1cxp  26861  cxploglim2  26865  jensenlem2  26874  emcllem6  26887  harmoniclbnd  26895  harmonicubnd  26896  harmonicbnd4  26897  fsumharmonic  26898  lgamgulmlem2  26916  lgamgulmlem3  26917  lgamgulmlem5  26919  lgambdd  26923  ftalem2  26960  basellem3  26969  basellem5  26971  basellem6  26972  dvdsflsumcom  27074  fsumfldivdiaglem  27075  ppiub  27091  chtublem  27098  logfac2  27104  chpub  27107  logfacubnd  27108  logfaclbnd  27109  logfacbnd3  27110  logexprlim  27112  bcmono  27164  bpos1lem  27169  bposlem1  27171  bposlem2  27172  bposlem3  27173  bposlem4  27174  bposlem5  27175  bposlem6  27176  bposlem7  27177  bposlem9  27179  lgsdirprm  27218  lgsquadlem1  27267  2lgslem1c  27280  2sqlem8  27313  chebbnd1lem1  27356  chebbnd1lem3  27358  chtppilimlem1  27360  chpchtlim  27366  vmadivsumb  27370  rplogsumlem1  27371  rplogsumlem2  27372  rpvmasumlem  27374  dchrisumlema  27375  dchrisumlem2  27377  dchrisumlem3  27378  dchrmusum2  27381  dchrvmasumlem2  27385  dchrvmasumlem3  27386  dchrvmasumlema  27387  dchrvmasumiflem1  27388  dchrisum0flblem1  27395  dchrisum0flblem2  27396  dchrisum0fno1  27398  dchrisum0re  27400  dchrisum0lem1b  27402  dchrisum0lem1  27403  dchrisum0lem2a  27404  dchrisum0  27407  rplogsum  27414  mudivsum  27417  mulogsumlem  27418  logdivsum  27420  mulog2sumlem1  27421  mulog2sumlem2  27422  2vmadivsumlem  27427  log2sumbnd  27431  selberglem2  27433  selbergb  27436  selberg2lem  27437  selberg2b  27439  chpdifbndlem1  27440  logdivbnd  27443  selberg3lem1  27444  selberg3lem2  27445  selberg4lem1  27447  pntrmax  27451  pntrsumo1  27452  pntrsumbnd  27453  pntrlog2bndlem1  27464  pntrlog2bndlem2  27465  pntrlog2bndlem3  27466  pntrlog2bndlem5  27468  pntrlog2bndlem6  27470  pntrlog2bnd  27471  pntpbnd1a  27472  pntpbnd1  27473  pntpbnd2  27474  pntibndlem2  27478  pntibndlem3  27479  pntlemg  27485  pntlemr  27489  pntlemj  27490  pntlemf  27492  pntlemk  27493  pntlemo  27494  pntleml  27498  abvcxp  27502  qabvle  27512  padicabv  27517  ostth2lem2  27521  ostth2lem3  27522  ostth3  27525  axlowdimlem16  28860  axcontlem8  28874  axcontlem10  28876  wwlksm1edg  29784  wwlksubclwwlk  29960  smcnlem  30599  nmoub3i  30675  ubthlem3  30774  minvecolem2  30777  minvecolem3  30778  minvecolem4  30782  htthlem  30819  bcs2  31084  pjhthlem1  31293  cnlnadjlem2  31970  cnlnadjlem7  31975  nmopadjlem  31991  nmoptrii  31996  nmopcoadji  32003  leopnmid  32040  cdj1i  32335  nndiffz1  32682  nexple  32742  oexpled  32745  pmtrto1cl  33029  psgnfzto1stlem  33030  fzto1st  33033  psgnfzto1st  33035  cyc3conja  33087  constrresqrtcl  33740  cos9thpiminplylem1  33745  smatrcl  33759  submateqlem1  33770  esumpcvgval  34041  oddpwdc  34318  eulerpartlems  34324  eulerpartlemgc  34326  eulerpartlemb  34332  dstfrvunirn  34439  orvclteinc  34440  ballotlemsima  34480  ballotlemfrcn0  34494  signstfveq0  34541  fsum2dsub  34571  breprexplemc  34596  breprexp  34597  logdivsqrle  34614  hgt750lemb  34620  hgt750leme  34622  tgoldbachgnn  34623  dnibndlem2  36440  dnibndlem6  36444  dnibndlem9  36447  dnibndlem10  36448  dnibndlem11  36449  dnibndlem12  36450  knoppcnlem4  36457  unblimceq0lem  36467  unblimceq0  36468  unbdqndv2lem2  36471  knoppndvlem11  36483  knoppndvlem14  36486  knoppndvlem15  36487  knoppndvlem18  36490  knoppndvlem21  36493  poimirlem6  37593  poimirlem7  37594  poimirlem13  37600  poimirlem15  37602  poimirlem29  37616  mblfinlem2  37625  mblfinlem3  37626  mblfinlem4  37627  ismblfin  37628  itg2addnc  37641  iblmulc2nc  37652  ftc1anclem7  37666  ftc1anclem8  37667  filbcmb  37707  geomcau  37726  prdsbnd  37760  cntotbnd  37763  bfplem2  37790  rrntotbnd  37803  iccbnd  37807  lcmineqlem20  42009  lcmineqlem21  42010  lcmineqlem22  42011  3lexlogpow5ineq2  42016  3lexlogpow5ineq5  42021  aks4d1p1p2  42031  aks4d1p1p4  42032  aks4d1p1p7  42035  aks4d1p1p5  42036  aks4d1p1  42037  aks4d1p2  42038  aks4d1p3  42039  aks4d1p5  42041  aks4d1p6  42042  aks4d1p7d1  42043  aks4d1p7  42044  aks4d1p8  42048  posbezout  42061  aks6d1c1  42077  aks6d1c2lem4  42088  2np3bcnp1  42105  sticksstones6  42112  sticksstones7  42113  sticksstones10  42116  sticksstones12a  42118  sticksstones12  42119  sticksstones22  42129  bcled  42139  bcle2d  42140  aks6d1c7lem1  42141  aks6d1c7lem2  42142  unitscyglem4  42159  lzunuz  42729  irrapxlem3  42785  irrapxlem4  42786  irrapxlem5  42787  pellexlem2  42791  pell1qrge1  42831  monotoddzzfi  42904  jm2.17a  42922  rmygeid  42926  fzmaxdif  42943  jm2.27c  42969  jm3.1lem1  42979  expdiophlem1  42983  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  imo72b2lem0  44127  int-ineqtransd  44156  dvgrat  44274  monoords  45268  absnpncan2d  45273  absnpncan3d  45278  ssfiunibd  45280  rexabslelem  45387  uzublem  45399  sqrlearg  45524  fmul01  45551  fmul01lt1lem1  45555  fmul01lt1lem2  45556  climsuselem1  45578  climsuse  45579  limsupresico  45671  limsupubuzlem  45683  limsupmnfuzlem  45697  limsupre3uzlem  45706  liminfresico  45742  limsup10exlem  45743  cnrefiisplem  45800  dvdivbd  45894  dvbdfbdioolem2  45900  ioodvbdlimc1lem1  45902  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvnmul  45914  dvnprodlem1  45917  dvnprodlem2  45918  iblspltprt  45944  itgspltprt  45950  stoweidlem1  45972  stoweidlem3  45974  stoweidlem5  45976  stoweidlem11  45982  stoweidlem17  45988  stoweidlem20  45991  stoweidlem26  45997  stoweidlem34  46005  wallispilem4  46039  stirlinglem11  46055  stirlinglem12  46056  stirlinglem13  46057  fourierdlem12  46090  fourierdlem15  46093  fourierdlem20  46098  fourierdlem30  46108  fourierdlem39  46117  fourierdlem42  46120  fourierdlem47  46124  fourierdlem50  46127  fourierdlem64  46141  fourierdlem65  46142  fourierdlem68  46145  fourierdlem73  46150  fourierdlem77  46154  fourierdlem79  46156  fourierdlem87  46164  elaa2lem  46204  etransclem23  46228  ioorrnopnlem  46275  salgencntex  46314  sge0le  46378  sge0isum  46398  sge0xaddlem1  46404  hoicvr  46519  hsphoidmvle2  46556  hoidmv1lelem1  46562  hoidmv1lelem2  46563  hoidmv1lelem3  46564  hoidmvlelem1  46566  hoidmvlelem2  46567  hoidmvlelem4  46569  hspmbllem1  46597  hspmbllem2  46598  smfmullem1  46762  smfmullem2  46763  smfmullem3  46764  smfsuplem1  46782  ormkglobd  46846  natglobalincr  46848  2ltceilhalf  47302  ceilhalfnn  47310  modmknepk  47336  lighneallem4a  47582  gpgusgralem  48020  gpgedgvtx1  48026  gpg3kgrtriexlem4  48050  gpg3kgrtriexlem6  48052  fllog2  48530  itcovalt2lem2lem1  48635