Theorem letrd 11447

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   class class class wbr 5166  ℝcr 11183   ≤ cle 11325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pow 5383  ax-pr 5447  ax-un 7770  ax-resscn 11241  ax-pre-lttri 11258  ax-pre-lttrn 11259

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-nel 3053  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580  df-fv 6581  df-er 8763  df-en 9004  df-dom 9005  df-sdom 9006  df-pnf 11326  df-mnf 11327  df-xr 11328  df-ltxr 11329  df-le 11330

This theorem is referenced by:  lesub3d  11908  supmul1  12264  supmul  12267  nn0negleid  12605  eluzuzle  12912  iccsplit  13545  supicc  13561  fzdisj  13611  ssfzunsnext  13629  difelfzle  13698  flwordi  13863  flleceil  13904  uzsup  13914  modltm1p1mod  13974  seqf1olem1  14092  zzlesq  14255  bernneq  14278  bernneq3  14280  discr1  14288  faclbnd  14339  faclbnd4lem1  14342  facubnd  14349  seqcoll  14513  01sqrexlem7  15297  absle  15364  releabs  15370  absrdbnd  15390  rexuzre  15401  limsupgre  15527  lo1bddrp  15571  rlimclim1  15591  rlimresb  15611  rlimrege0  15625  o1add  15660  o1sub  15662  climsqz  15687  climsqz2  15688  rlimsqzlem  15697  rlimsqz  15698  rlimsqz2  15699  rlimno1  15702  isercoll  15716  caucvgrlem  15721  iseraltlem3  15732  o1fsum  15861  cvgcmp  15864  cvgcmpce  15866  climcnds  15899  expcnv  15912  cvgrat  15931  mertenslem2  15933  fprodle  16044  eftlub  16157  rpnnen2lem12  16273  bitsfzo  16481  isprm5  16754  isprm7  16755  eulerthlem2  16829  pcmpt2  16940  pcfac  16946  prmreclem3  16965  prmreclem4  16966  prmreclem5  16967  4sqlem11  17002  vdwlem1  17028  vdwlem3  17030  setsstruct2  17221  prdsxmetlem  24399  nrmmetd  24608  nm2dif  24659  nlmvscnlem2  24727  nmoco  24779  nmotri  24781  nghmcn  24787  icccmplem2  24864  reconnlem2  24868  elii1  24983  xrhmeo  24996  cnheiborlem  25005  bndth  25009  tcphcphlem1  25288  ipcnlem2  25297  cncmet  25375  trirn  25453  minveclem2  25479  minveclem4  25485  ivthlem2  25506  ovolunlem1a  25550  ovolunlem1  25551  ovolfiniun  25555  ovoliunlem1  25556  ovolicc2lem4  25574  ovolicc2lem5  25575  ovolicopnf  25578  nulmbl2  25590  ioombl1lem4  25615  ioorcl2  25626  uniioombllem3  25639  uniioombllem4  25640  uniioombllem5  25641  volcn  25660  vitalilem2  25663  vitali  25667  mbfi1fseqlem5  25774  mbfi1fseqlem6  25775  itg2splitlem  25803  itg2monolem1  25805  itg2monolem3  25807  itg2mono  25808  itg2cnlem1  25816  itgle  25865  bddmulibl  25894  bddiblnc  25897  ditgsplitlem  25915  dveflem  26037  dvlip  26052  dveq0  26059  dvfsumabs  26083  dvfsumlem1  26086  dvfsumlem2  26087  dvfsumlem2OLD  26088  dvfsumlem3  26089  dvfsumlem4  26090  dvfsum2  26095  fta1glem2  26228  dgradd2  26328  plydiveu  26358  fta1lem  26367  aalioulem2  26393  aalioulem3  26394  aalioulem4  26395  aalioulem5  26396  aaliou3lem8  26405  aaliou3lem9  26410  ulmbdd  26459  ulmcn  26460  mtest  26465  mtestbdd  26466  abelthlem2  26494  abelthlem7  26500  pilem2  26514  tanabsge  26566  cosordlem  26590  tanord  26598  logneg2  26675  abslogle  26678  dvlog2lem  26712  cxple2a  26759  abscxpbnd  26814  atans2  26992  leibpi  27003  o1cxp  27036  cxploglim2  27040  jensenlem2  27049  emcllem6  27062  harmoniclbnd  27070  harmonicubnd  27071  harmonicbnd4  27072  fsumharmonic  27073  lgamgulmlem2  27091  lgamgulmlem3  27092  lgamgulmlem5  27094  lgambdd  27098  ftalem2  27135  basellem3  27144  basellem5  27146  basellem6  27147  dvdsflsumcom  27249  fsumfldivdiaglem  27250  ppiub  27266  chtublem  27273  logfac2  27279  chpub  27282  logfacubnd  27283  logfaclbnd  27284  logfacbnd3  27285  logexprlim  27287  bcmono  27339  bpos1lem  27344  bposlem1  27346  bposlem2  27347  bposlem3  27348  bposlem4  27349  bposlem5  27350  bposlem6  27351  bposlem7  27352  bposlem9  27354  lgsdirprm  27393  lgsquadlem1  27442  2lgslem1c  27455  2sqlem8  27488  chebbnd1lem1  27531  chebbnd1lem3  27533  chtppilimlem1  27535  chpchtlim  27541  vmadivsumb  27545  rplogsumlem1  27546  rplogsumlem2  27547  rpvmasumlem  27549  dchrisumlema  27550  dchrisumlem2  27552  dchrisumlem3  27553  dchrmusum2  27556  dchrvmasumlem2  27560  dchrvmasumlem3  27561  dchrvmasumlema  27562  dchrvmasumiflem1  27563  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0fno1  27573  dchrisum0re  27575  dchrisum0lem1b  27577  dchrisum0lem1  27578  dchrisum0lem2a  27579  dchrisum0  27582  rplogsum  27589  mudivsum  27592  mulogsumlem  27593  logdivsum  27595  mulog2sumlem1  27596  mulog2sumlem2  27597  2vmadivsumlem  27602  log2sumbnd  27606  selberglem2  27608  selbergb  27611  selberg2lem  27612  selberg2b  27614  chpdifbndlem1  27615  logdivbnd  27618  selberg3lem1  27619  selberg3lem2  27620  selberg4lem1  27622  pntrmax  27626  pntrsumo1  27627  pntrsumbnd  27628  pntrlog2bndlem1  27639  pntrlog2bndlem2  27640  pntrlog2bndlem3  27641  pntrlog2bndlem5  27643  pntrlog2bndlem6  27645  pntrlog2bnd  27646  pntpbnd1a  27647  pntpbnd1  27648  pntpbnd2  27649  pntibndlem2  27653  pntibndlem3  27654  pntlemg  27660  pntlemr  27664  pntlemj  27665  pntlemf  27667  pntlemk  27668  pntlemo  27669  pntleml  27673  abvcxp  27677  qabvle  27687  padicabv  27692  ostth2lem2  27696  ostth2lem3  27697  ostth3  27700  axlowdimlem16  28990  axcontlem8  29004  axcontlem10  29006  wwlksm1edg  29914  wwlksubclwwlk  30090  smcnlem  30729  nmoub3i  30805  ubthlem3  30904  minvecolem2  30907  minvecolem3  30908  minvecolem4  30912  htthlem  30949  bcs2  31214  pjhthlem1  31423  cnlnadjlem2  32100  cnlnadjlem7  32105  nmopadjlem  32121  nmoptrii  32126  nmopcoadji  32133  leopnmid  32170  cdj1i  32465  nndiffz1  32791  pmtrto1cl  33092  psgnfzto1stlem  33093  fzto1st  33096  psgnfzto1st  33098  cyc3conja  33150  smatrcl  33742  submateqlem1  33753  nexple  33973  esumpcvgval  34042  oddpwdc  34319  eulerpartlems  34325  eulerpartlemgc  34327  eulerpartlemb  34333  dstfrvunirn  34439  orvclteinc  34440  ballotlemsima  34480  ballotlemfrcn0  34494  signstfveq0  34554  fsum2dsub  34584  breprexplemc  34609  breprexp  34610  logdivsqrle  34627  hgt750lemb  34633  hgt750leme  34635  tgoldbachgnn  34636  dnibndlem2  36445  dnibndlem6  36449  dnibndlem9  36452  dnibndlem10  36453  dnibndlem11  36454  dnibndlem12  36455  knoppcnlem4  36462  unblimceq0lem  36472  unblimceq0  36473  unbdqndv2lem2  36476  knoppndvlem11  36488  knoppndvlem14  36491  knoppndvlem15  36492  knoppndvlem18  36495  knoppndvlem21  36498  poimirlem6  37586  poimirlem7  37587  poimirlem13  37593  poimirlem15  37595  poimirlem29  37609  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  itg2addnc  37634  iblmulc2nc  37645  ftc1anclem7  37659  ftc1anclem8  37660  filbcmb  37700  geomcau  37719  prdsbnd  37753  cntotbnd  37756  bfplem2  37783  rrntotbnd  37796  iccbnd  37800  lcmineqlem20  42005  lcmineqlem21  42006  lcmineqlem22  42007  3lexlogpow5ineq2  42012  3lexlogpow5ineq5  42017  aks4d1p1p2  42027  aks4d1p1p4  42028  aks4d1p1p7  42031  aks4d1p1p5  42032  aks4d1p1  42033  aks4d1p2  42034  aks4d1p3  42035  aks4d1p5  42037  aks4d1p6  42038  aks4d1p7d1  42039  aks4d1p7  42040  aks4d1p8  42044  posbezout  42057  aks6d1c1  42073  aks6d1c2lem4  42084  2np3bcnp1  42101  sticksstones6  42108  sticksstones7  42109  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  bcled  42135  bcle2d  42136  aks6d1c7lem1  42137  aks6d1c7lem2  42138  unitscyglem4  42155  metakunt1  42162  metakunt12  42173  metakunt28  42189  lzunuz  42724  irrapxlem3  42780  irrapxlem4  42781  irrapxlem5  42782  pellexlem2  42786  pell1qrge1  42826  monotoddzzfi  42899  jm2.17a  42917  rmygeid  42921  fzmaxdif  42938  jm2.27c  42964  jm3.1lem1  42974  expdiophlem1  42978  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  imo72b2lem0  44127  int-ineqtransd  44156  dvgrat  44281  monoords  45212  absnpncan2d  45217  absnpncan3d  45222  ssfiunibd  45224  leadd12dd  45231  rexabslelem  45333  uzublem  45345  sqrlearg  45471  fmul01  45501  fmul01lt1lem1  45505  fmul01lt1lem2  45506  climsuselem1  45528  climsuse  45529  limsupresico  45621  limsupubuzlem  45633  limsupmnfuzlem  45647  limsupre3uzlem  45656  liminfresico  45692  limsup10exlem  45693  cnrefiisplem  45750  dvdivbd  45844  dvbdfbdioolem2  45850  ioodvbdlimc1lem1  45852  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  iblspltprt  45894  itgspltprt  45900  stoweidlem1  45922  stoweidlem3  45924  stoweidlem5  45926  stoweidlem11  45932  stoweidlem17  45938  stoweidlem20  45941  stoweidlem26  45947  stoweidlem34  45955  wallispilem4  45989  stirlinglem11  46005  stirlinglem12  46006  stirlinglem13  46007  fourierdlem12  46040  fourierdlem15  46043  fourierdlem20  46048  fourierdlem30  46058  fourierdlem39  46067  fourierdlem42  46070  fourierdlem47  46074  fourierdlem50  46077  fourierdlem64  46091  fourierdlem65  46092  fourierdlem68  46095  fourierdlem73  46100  fourierdlem77  46104  fourierdlem79  46106  fourierdlem87  46114  elaa2lem  46154  etransclem23  46178  ioorrnopnlem  46225  salgencntex  46264  sge0le  46328  sge0isum  46348  sge0xaddlem1  46354  hoicvr  46469  hsphoidmvle2  46506  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem4  46519  hspmbllem1  46547  hspmbllem2  46548  smfmullem1  46712  smfmullem2  46713  smfmullem3  46714  smfsuplem1  46732  natglobalincr  46796  lighneallem4a  47482  fllog2  48302  itcovalt2lem2lem1  48407