Theorem letrd 11415

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105   class class class wbr 5147  ℝcr 11151   ≤ cle 11293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-resscn 11209  ax-pre-lttri 11226  ax-pre-lttrn 11227

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298

This theorem is referenced by:  lesub3d  11878  supmul1  12234  supmul  12237  nn0negleid  12575  eluzuzle  12884  iccsplit  13521  supicc  13537  fzdisj  13587  ssfzunsnext  13605  difelfzle  13677  flwordi  13848  flleceil  13889  uzsup  13899  modltm1p1mod  13960  seqf1olem1  14078  zzlesq  14241  bernneq  14264  bernneq3  14266  discr1  14274  faclbnd  14325  faclbnd4lem1  14328  facubnd  14335  seqcoll  14499  01sqrexlem7  15283  absle  15350  releabs  15356  absrdbnd  15376  rexuzre  15387  limsupgre  15513  lo1bddrp  15557  rlimclim1  15577  rlimresb  15597  rlimrege0  15611  o1add  15646  o1sub  15648  climsqz  15673  climsqz2  15674  rlimsqzlem  15681  rlimsqz  15682  rlimsqz2  15683  rlimno1  15686  isercoll  15700  caucvgrlem  15705  iseraltlem3  15716  o1fsum  15845  cvgcmp  15848  cvgcmpce  15850  climcnds  15883  expcnv  15896  cvgrat  15915  mertenslem2  15917  fprodle  16028  eftlub  16141  rpnnen2lem12  16257  bitsfzo  16468  isprm5  16740  isprm7  16741  eulerthlem2  16815  pcmpt2  16926  pcfac  16932  prmreclem3  16951  prmreclem4  16952  prmreclem5  16953  4sqlem11  16988  vdwlem1  17014  vdwlem3  17016  setsstruct2  17207  prdsxmetlem  24393  nrmmetd  24602  nm2dif  24653  nlmvscnlem2  24721  nmoco  24773  nmotri  24775  nghmcn  24781  icccmplem2  24858  reconnlem2  24862  elii1  24977  xrhmeo  24990  cnheiborlem  24999  bndth  25003  tcphcphlem1  25282  ipcnlem2  25291  cncmet  25369  trirn  25447  minveclem2  25473  minveclem4  25479  ivthlem2  25500  ovolunlem1a  25544  ovolunlem1  25545  ovolfiniun  25549  ovoliunlem1  25550  ovolicc2lem4  25568  ovolicc2lem5  25569  ovolicopnf  25572  nulmbl2  25584  ioombl1lem4  25609  ioorcl2  25620  uniioombllem3  25633  uniioombllem4  25634  uniioombllem5  25635  volcn  25654  vitalilem2  25657  vitali  25661  mbfi1fseqlem5  25768  mbfi1fseqlem6  25769  itg2splitlem  25797  itg2monolem1  25799  itg2monolem3  25801  itg2mono  25802  itg2cnlem1  25810  itgle  25859  bddmulibl  25888  bddiblnc  25891  ditgsplitlem  25909  dveflem  26031  dvlip  26046  dveq0  26053  dvfsumabs  26077  dvfsumlem1  26080  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumlem3  26083  dvfsumlem4  26084  dvfsum2  26089  fta1glem2  26222  dgradd2  26322  plydiveu  26354  fta1lem  26363  aalioulem2  26389  aalioulem3  26390  aalioulem4  26391  aalioulem5  26392  aaliou3lem8  26401  aaliou3lem9  26406  ulmbdd  26455  ulmcn  26456  mtest  26461  mtestbdd  26462  abelthlem2  26490  abelthlem7  26496  pilem2  26510  tanabsge  26562  cosordlem  26586  tanord  26594  logneg2  26671  abslogle  26674  dvlog2lem  26708  cxple2a  26755  abscxpbnd  26810  atans2  26988  leibpi  26999  o1cxp  27032  cxploglim2  27036  jensenlem2  27045  emcllem6  27058  harmoniclbnd  27066  harmonicubnd  27067  harmonicbnd4  27068  fsumharmonic  27069  lgamgulmlem2  27087  lgamgulmlem3  27088  lgamgulmlem5  27090  lgambdd  27094  ftalem2  27131  basellem3  27140  basellem5  27142  basellem6  27143  dvdsflsumcom  27245  fsumfldivdiaglem  27246  ppiub  27262  chtublem  27269  logfac2  27275  chpub  27278  logfacubnd  27279  logfaclbnd  27280  logfacbnd3  27281  logexprlim  27283  bcmono  27335  bpos1lem  27340  bposlem1  27342  bposlem2  27343  bposlem3  27344  bposlem4  27345  bposlem5  27346  bposlem6  27347  bposlem7  27348  bposlem9  27350  lgsdirprm  27389  lgsquadlem1  27438  2lgslem1c  27451  2sqlem8  27484  chebbnd1lem1  27527  chebbnd1lem3  27529  chtppilimlem1  27531  chpchtlim  27537  vmadivsumb  27541  rplogsumlem1  27542  rplogsumlem2  27543  rpvmasumlem  27545  dchrisumlema  27546  dchrisumlem2  27548  dchrisumlem3  27549  dchrmusum2  27552  dchrvmasumlem2  27556  dchrvmasumlem3  27557  dchrvmasumlema  27558  dchrvmasumiflem1  27559  dchrisum0flblem1  27566  dchrisum0flblem2  27567  dchrisum0fno1  27569  dchrisum0re  27571  dchrisum0lem1b  27573  dchrisum0lem1  27574  dchrisum0lem2a  27575  dchrisum0  27578  rplogsum  27585  mudivsum  27588  mulogsumlem  27589  logdivsum  27591  mulog2sumlem1  27592  mulog2sumlem2  27593  2vmadivsumlem  27598  log2sumbnd  27602  selberglem2  27604  selbergb  27607  selberg2lem  27608  selberg2b  27610  chpdifbndlem1  27611  logdivbnd  27614  selberg3lem1  27615  selberg3lem2  27616  selberg4lem1  27618  pntrmax  27622  pntrsumo1  27623  pntrsumbnd  27624  pntrlog2bndlem1  27635  pntrlog2bndlem2  27636  pntrlog2bndlem3  27637  pntrlog2bndlem5  27639  pntrlog2bndlem6  27641  pntrlog2bnd  27642  pntpbnd1a  27643  pntpbnd1  27644  pntpbnd2  27645  pntibndlem2  27649  pntibndlem3  27650  pntlemg  27656  pntlemr  27660  pntlemj  27661  pntlemf  27663  pntlemk  27664  pntlemo  27665  pntleml  27669  abvcxp  27673  qabvle  27683  padicabv  27688  ostth2lem2  27692  ostth2lem3  27693  ostth3  27696  axlowdimlem16  28986  axcontlem8  29000  axcontlem10  29002  wwlksm1edg  29910  wwlksubclwwlk  30086  smcnlem  30725  nmoub3i  30801  ubthlem3  30900  minvecolem2  30903  minvecolem3  30904  minvecolem4  30908  htthlem  30945  bcs2  31210  pjhthlem1  31419  cnlnadjlem2  32096  cnlnadjlem7  32101  nmopadjlem  32117  nmoptrii  32122  nmopcoadji  32129  leopnmid  32166  cdj1i  32461  nndiffz1  32794  pmtrto1cl  33101  psgnfzto1stlem  33102  fzto1st  33105  psgnfzto1st  33107  cyc3conja  33159  smatrcl  33756  submateqlem1  33767  nexple  33989  esumpcvgval  34058  oddpwdc  34335  eulerpartlems  34341  eulerpartlemgc  34343  eulerpartlemb  34349  dstfrvunirn  34455  orvclteinc  34456  ballotlemsima  34496  ballotlemfrcn0  34510  signstfveq0  34570  fsum2dsub  34600  breprexplemc  34625  breprexp  34626  logdivsqrle  34643  hgt750lemb  34649  hgt750leme  34651  tgoldbachgnn  34652  dnibndlem2  36461  dnibndlem6  36465  dnibndlem9  36468  dnibndlem10  36469  dnibndlem11  36470  dnibndlem12  36471  knoppcnlem4  36478  unblimceq0lem  36488  unblimceq0  36489  unbdqndv2lem2  36492  knoppndvlem11  36504  knoppndvlem14  36507  knoppndvlem15  36508  knoppndvlem18  36511  knoppndvlem21  36514  poimirlem6  37612  poimirlem7  37613  poimirlem13  37619  poimirlem15  37621  poimirlem29  37635  mblfinlem2  37644  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  itg2addnc  37660  iblmulc2nc  37671  ftc1anclem7  37685  ftc1anclem8  37686  filbcmb  37726  geomcau  37745  prdsbnd  37779  cntotbnd  37782  bfplem2  37809  rrntotbnd  37822  iccbnd  37826  lcmineqlem20  42029  lcmineqlem21  42030  lcmineqlem22  42031  3lexlogpow5ineq2  42036  3lexlogpow5ineq5  42041  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p2  42058  aks4d1p3  42059  aks4d1p5  42061  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8  42068  posbezout  42081  aks6d1c1  42097  aks6d1c2lem4  42108  2np3bcnp1  42125  sticksstones6  42132  sticksstones7  42133  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  aks6d1c7lem2  42162  unitscyglem4  42179  metakunt1  42186  metakunt12  42197  metakunt28  42213  lzunuz  42755  irrapxlem3  42811  irrapxlem4  42812  irrapxlem5  42813  pellexlem2  42817  pell1qrge1  42857  monotoddzzfi  42930  jm2.17a  42948  rmygeid  42952  fzmaxdif  42969  jm2.27c  42995  jm3.1lem1  43005  expdiophlem1  43009  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  imo72b2lem0  44154  int-ineqtransd  44183  dvgrat  44307  monoords  45247  absnpncan2d  45252  absnpncan3d  45257  ssfiunibd  45259  leadd12dd  45266  rexabslelem  45367  uzublem  45379  sqrlearg  45505  fmul01  45535  fmul01lt1lem1  45539  fmul01lt1lem2  45540  climsuselem1  45562  climsuse  45563  limsupresico  45655  limsupubuzlem  45667  limsupmnfuzlem  45681  limsupre3uzlem  45690  liminfresico  45726  limsup10exlem  45727  cnrefiisplem  45784  dvdivbd  45878  dvbdfbdioolem2  45884  ioodvbdlimc1lem1  45886  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnmul  45898  dvnprodlem1  45901  dvnprodlem2  45902  iblspltprt  45928  itgspltprt  45934  stoweidlem1  45956  stoweidlem3  45958  stoweidlem5  45960  stoweidlem11  45966  stoweidlem17  45972  stoweidlem20  45975  stoweidlem26  45981  stoweidlem34  45989  wallispilem4  46023  stirlinglem11  46039  stirlinglem12  46040  stirlinglem13  46041  fourierdlem12  46074  fourierdlem15  46077  fourierdlem20  46082  fourierdlem30  46092  fourierdlem39  46101  fourierdlem42  46104  fourierdlem47  46108  fourierdlem50  46111  fourierdlem64  46125  fourierdlem65  46126  fourierdlem68  46129  fourierdlem73  46134  fourierdlem77  46138  fourierdlem79  46140  fourierdlem87  46148  elaa2lem  46188  etransclem23  46212  ioorrnopnlem  46259  salgencntex  46298  sge0le  46362  sge0isum  46382  sge0xaddlem1  46388  hoicvr  46503  hsphoidmvle2  46540  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem4  46553  hspmbllem1  46581  hspmbllem2  46582  smfmullem1  46746  smfmullem2  46747  smfmullem3  46748  smfsuplem1  46766  natglobalincr  46830  lighneallem4a  47532  gpgusgralem  47945  2ltceilhalf  47949  gpgedgvtx1  47954  gpg3nbgrvtxlem  47957  fllog2  48417  itcovalt2lem2lem1  48522