Theorem letrd 11506

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   class class class wbr 5108  ℝcr 11238   ≤ cle 11383

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-resscn 11296  ax-pre-lttri 11313  ax-pre-lttrn 11314

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-er 8755  df-en 9012  df-dom 9013  df-sdom 9014  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388

This theorem is used by:  lesub3d  11974  le2addd  11975  supmul1  12326  supmul  12329  nn0negleid  12698  eluzuzle  13014  iccsplit  13656  supicc  13672  fzdisj  13725  ssfzunsnext  13743  difelfzle  13815  flwordi  13992  flleceil  14033  uzsup  14043  modltm1p1mod  14106  seqf1olem1  14224  zzlesq  14390  bernneq  14414  bernneq3  14416  discr1  14424  faclbnd  14475  faclbnd4lem1  14478  facubnd  14485  seqcoll  14650  01sqrexlem7  15458  absle  15526  releabs  15532  absrdbnd  15553  rexuzre  15564  limsupgre  15692  lo1bddrp  15736  rlimclim1  15756  rlimresb  15776  rlimrege0  15790  o1add  15825  o1sub  15827  climsqz  15852  climsqz2  15853  rlimsqzlem  15860  rlimsqz  15861  rlimsqz2  15862  rlimno1  15865  isercoll  15879  caucvgrlem  15884  iseraltlem3  15895  o1fsum  16024  cvgcmp  16027  cvgcmpce  16029  climcnds  16064  expcnv  16077  cvgrat  16096  mertenslem2  16098  fprodle  16207  eftlub  16321  rpnnen2lem12  16437  bitsfzo  16649  isprm5  16927  isprm7  16928  eulerthlem2  17003  pcmpt2  17115  pcfac  17121  prmreclem3  17140  prmreclem4  17141  prmreclem5  17142  4sqlem11  17177  vdwlem1  17203  vdwlem3  17205  setsstruct2  17396  prdsxmetlem  24742  nrmmetd  24948  nm2dif  24999  nlmvscnlem2  25059  nmoco  25111  nmotri  25113  nghmcn  25119  icccmplem2  25198  reconnlem2  25202  elii1  25311  xrhmeo  25322  cnheiborlem  25330  bndth  25334  tcphcphlem1  25611  ipcnlem2  25620  cncmet  25698  trirn  25776  minveclem2  25802  minveclem4  25808  ivthlem2  25828  ovolunlem1a  25872  ovolunlem1  25873  ovolfiniun  25877  ovoliunlem1  25878  ovolicc2lem4  25896  ovolicc2lem5  25897  ovolicopnf  25900  nulmbl2  25912  ioombl1lem4  25937  ioorcl2  25948  uniioombllem3  25961  uniioombllem4  25962  uniioombllem5  25963  volcn  25982  vitalilem2  25985  vitali  25989  mbfi1fseqlem5  26095  mbfi1fseqlem6  26096  itg2splitlem  26124  itg2monolem1  26126  itg2monolem3  26128  itg2mono  26129  itg2cnlem1  26137  itgle  26185  bddmulibl  26214  bddiblnc  26217  ditgsplitlem  26235  dveflem  26354  dvlip  26368  dveq0  26375  dvfsumabs  26398  dvfsumlem1  26401  dvfsumlem2  26402  dvfsumlem3  26403  dvfsumlem4  26404  dvfsum2  26409  fta1glem2  26542  dgradd2  26642  plydiveu  26674  fta1lem  26683  aalioulem2  26717  aalioulem3  26718  aalioulem4  26719  aalioulem5  26720  aaliou3lem8  26729  aaliou3lem9  26734  ulmbdd  26782  ulmcn  26783  mtest  26788  mtestbdd  26789  abelthlem2  26816  abelthlem7  26822  pilem2  26836  tanabsge  26892  cosordlem  26915  tanord  26923  logneg2  27000  abslogle  27003  dvlog2lem  27037  cxple2a  27084  abscxpbnd  27138  atans2  27316  leibpi  27327  o1cxp  27359  cxploglim2  27363  jensenlem2  27372  emcllem6  27385  harmoniclbnd  27393  harmonicubnd  27394  harmonicbnd4  27395  fsumharmonic  27396  lgamgulmlem2  27414  lgamgulmlem3  27415  lgamgulmlem5  27417  lgambdd  27421  ftalem2  27458  basellem3  27467  basellem5  27469  basellem6  27470  dvdsflsumcom  27572  fsumfldivdiaglem  27573  ppiub  27588  chtublem  27595  logfac2  27601  chpub  27604  logfacubnd  27605  logfaclbnd  27606  logfacbnd3  27607  logexprlim  27609  bcmono  27661  bpos1lem  27666  bposlem1  27668  bposlem2  27669  bposlem3  27670  bposlem4  27671  bposlem5  27672  bposlem6  27673  bposlem7  27674  bposlem9  27676  lgsdirprm  27715  lgsquadlem1  27764  2lgslem1c  27777  2sqlem8  27810  chebbnd1lem1  27853  chebbnd1lem3  27855  chtppilimlem1  27857  chpchtlim  27863  vmadivsumb  27867  rplogsumlem1  27868  rplogsumlem2  27869  rpvmasumlem  27871  dchrisumlema  27872  dchrisumlem2  27874  dchrisumlem3  27875  dchrmusum2  27878  dchrvmasumlem2  27882  dchrvmasumlem3  27883  dchrvmasumlema  27884  dchrvmasumiflem1  27885  dchrisum0flblem1  27892  dchrisum0flblem2  27893  dchrisum0fno1  27895  dchrisum0re  27897  dchrisum0lem1b  27899  dchrisum0lem1  27900  dchrisum0lem2a  27901  dchrisum0  27904  rplogsum  27911  mudivsum  27914  mulogsumlem  27915  logdivsum  27917  mulog2sumlem1  27918  mulog2sumlem2  27919  2vmadivsumlem  27924  log2sumbnd  27928  selberglem2  27930  selbergb  27933  selberg2lem  27934  selberg2b  27936  chpdifbndlem1  27937  logdivbnd  27940  selberg3lem1  27941  selberg3lem2  27942  selberg4lem1  27944  pntrmax  27948  pntrsumo1  27949  pntrsumbnd  27950  pntrlog2bndlem1  27961  pntrlog2bndlem2  27962  pntrlog2bndlem3  27963  pntrlog2bndlem5  27965  pntrlog2bndlem6  27967  pntrlog2bnd  27968  pntpbnd1a  27969  pntpbnd1  27970  pntpbnd2  27971  pntibndlem2  27975  pntibndlem3  27976  pntlemg  27982  pntlemr  27986  pntlemj  27987  pntlemf  27989  pntlemk  27990  pntlemo  27991  pntleml  27995  abvcxp  27999  qabvle  28009  padicabv  28014  ostth2lem2  28018  ostth2lem3  28019  ostth3  28022  axlowdimlem16  29592  axcontlem8  29606  axcontlem10  29608  wwlksm1edg  30527  wwlksubclwwlk  30706  smcnlem  31356  nmoub3i  31432  ubthlem3  31531  minvecolem2  31534  minvecolem3  31535  minvecolem4  31539  htthlem  31576  bcs2  31841  pjhthlem1  32050  cnlnadjlem2  32727  cnlnadjlem7  32732  nmopadjlem  32748  nmoptrii  32753  nmopcoadji  32760  leopnmid  32797  cdj1i  33092  nndiffz1  33474  nexple  33520  oexpled  33523  pmtrto1cl  33759  psgnfzto1stlem  33760  fzto1st  33763  psgnfzto1st  33765  cyc3conja  33817  constrresqrtcl  34520  cos9thpiminplylem1  34525  smatrcl  34539  submateqlem1  34550  esumpcvgval  34821  oddpwdc  35097  eulerpartlems  35103  eulerpartlemgc  35105  eulerpartlemb  35111  dstfrvunirn  35218  orvclteinc  35219  ballotlemsima  35259  ballotlemfrcn0  35273  signstfveq0  35317  fsum2dsub  35347  breprexplemc  35372  breprexp  35373  logdivsqrle  35390  hgt750lemb  35396  hgt750leme  35398  tgoldbachgnn  35399  dnibndlem2  37560  dnibndlem6  37564  dnibndlem9  37567  dnibndlem10  37568  dnibndlem11  37569  dnibndlem12  37570  knoppcnlem4  37577  unblimceq0lem  37587  unblimceq0  37588  unbdqndv2lem2  37591  knoppndvlem11  37603  knoppndvlem14  37606  knoppndvlem15  37607  knoppndvlem18  37610  knoppndvlem21  37613  poimirlem6  38812  poimirlem7  38813  poimirlem13  38819  poimirlem15  38821  poimirlem29  38835  mblfinlem2  38844  mblfinlem3  38845  mblfinlem4  38846  ismblfin  38847  itg2addnc  38860  iblmulc2nc  38871  ftc1anclem7  38885  ftc1anclem8  38886  filbcmb  38940  geomcau  38959  prdsbnd  38993  cntotbnd  38996  bfplem2  39023  rrntotbnd  39036  iccbnd  39040  lcmineqlem20  43364  lcmineqlem21  43365  lcmineqlem22  43366  3lexlogpow5ineq2  43371  3lexlogpow5ineq5  43376  aks4d1p1p2  43386  aks4d1p1p4  43387  aks4d1p1p7  43390  aks4d1p1p5  43391  aks4d1p1  43392  aks4d1p2  43393  aks4d1p3  43394  aks4d1p5  43396  aks4d1p6  43397  aks4d1p7d1  43398  aks4d1p7  43399  aks4d1p8  43403  posbezout  43416  aks6d1c1  43432  aks6d1c2lem4  43443  2np3bcnp1  43460  sticksstones6  43467  sticksstones7  43468  sticksstones10  43471  sticksstones12a  43473  sticksstones12  43474  sticksstones22  43484  bcled  43494  bcle2d  43495  aks6d1c7lem1  43496  aks6d1c7lem2  43497  unitscyglem4  43514  lzunuz  44045  irrapxlem3  44097  irrapxlem4  44098  irrapxlem5  44099  pellexlem2  44103  pell1qrge1  44143  monotoddzzfi  44215  jm2.17a  44233  rmygeid  44237  fzmaxdif  44254  jm2.27c  44280  jm3.1lem1  44290  expdiophlem1  44294  fzunt  44717  fzuntd  44718  fzunt1d  44719  fzuntgd  44720  imo72b2lem0  45426  int-ineqtransd  45455  dvgrat  45557  monoords  46586  absnpncan2d  46591  absnpncan3d  46596  ssfiunibd  46598  rexabslelem  46701  uzublem  46713  sqrlearg  46838  fmul01  46865  fmul01lt1lem1  46869  fmul01lt1lem2  46870  climsuselem1  46892  climsuse  46893  limsupresico  46983  limsupubuzlem  46995  limsupmnfuzlem  47009  limsupre3uzlem  47018  liminfresico  47054  limsup10exlem  47055  cnrefiisplem  47112  dvdivbd  47206  dvbdfbdioolem2  47212  ioodvbdlimc1lem1  47214  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnmul  47226  dvnprodlem1  47229  dvnprodlem2  47230  iblspltprt  47256  itgspltprt  47262  stoweidlem1  47284  stoweidlem3  47286  stoweidlem5  47288  stoweidlem11  47294  stoweidlem17  47300  stoweidlem20  47303  stoweidlem26  47309  stoweidlem34  47317  wallispilem4  47351  stirlinglem11  47367  stirlinglem12  47368  stirlinglem13  47369  fourierdlem12  47402  fourierdlem15  47405  fourierdlem20  47410  fourierdlem30  47420  fourierdlem39  47429  fourierdlem42  47432  fourierdlem47  47436  fourierdlem50  47439  fourierdlem64  47453  fourierdlem65  47454  fourierdlem68  47457  fourierdlem73  47462  fourierdlem77  47466  fourierdlem79  47468  fourierdlem87  47476  elaa2lem  47516  etransclem23  47540  ioorrnopnlem  47587  salgencntex  47626  sge0le  47690  sge0isum  47710  sge0xaddlem1  47716  hoicvr  47831  hsphoidmvle2  47868  hoidmv1lelem1  47874  hoidmv1lelem2  47875  hoidmv1lelem3  47876  hoidmvlelem1  47878  hoidmvlelem2  47879  hoidmvlelem4  47881  hspmbllem1  47909  hspmbllem2  47910  smfmullem1  48074  smfmullem2  48075  smfmullem3  48076  smfsuplem1  48094  ormkglobd  48160  2ltceilhalf  48675  ceilhalfnn  48683  modmknepk  48711  lighneallem4a  48966  nprmdvdsfacm1lem4  48981  gpgusgralem  49427  gpgedgvtx1  49433  gpg3kgrtriexlem4  49457  gpg3kgrtriexlem6  49459  fllog2  50011  itcovalt2lem2lem1  50116