Theorem letrd 11297

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ℝcr 11031   ≤ cle 11174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5303  ax-pr 5371  ax-un 7683  ax-resscn 11089  ax-pre-lttri 11106  ax-pre-lttrn 11107

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-er 8637  df-en 8888  df-dom 8889  df-sdom 8890  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179

This theorem is referenced by:  lesub3d  11762  le2addd  11763  supmul1  12119  supmul  12122  nn0negleid  12483  eluzuzle  12791  iccsplit  13432  supicc  13448  fzdisj  13499  ssfzunsnext  13517  difelfzle  13589  flwordi  13765  flleceil  13806  uzsup  13816  modltm1p1mod  13879  seqf1olem1  13997  zzlesq  14162  bernneq  14185  bernneq3  14187  discr1  14195  faclbnd  14246  faclbnd4lem1  14249  facubnd  14256  seqcoll  14420  01sqrexlem7  15204  absle  15272  releabs  15278  absrdbnd  15298  rexuzre  15309  limsupgre  15437  lo1bddrp  15481  rlimclim1  15501  rlimresb  15521  rlimrege0  15535  o1add  15570  o1sub  15572  climsqz  15597  climsqz2  15598  rlimsqzlem  15605  rlimsqz  15606  rlimsqz2  15607  rlimno1  15610  isercoll  15624  caucvgrlem  15629  iseraltlem3  15640  o1fsum  15770  cvgcmp  15773  cvgcmpce  15775  climcnds  15810  expcnv  15823  cvgrat  15842  mertenslem2  15844  fprodle  15955  eftlub  16070  rpnnen2lem12  16186  bitsfzo  16398  isprm5  16671  isprm7  16672  eulerthlem2  16746  pcmpt2  16858  pcfac  16864  prmreclem3  16883  prmreclem4  16884  prmreclem5  16885  4sqlem11  16920  vdwlem1  16946  vdwlem3  16948  setsstruct2  17138  prdsxmetlem  24346  nrmmetd  24552  nm2dif  24603  nlmvscnlem2  24663  nmoco  24715  nmotri  24717  nghmcn  24723  icccmplem2  24802  reconnlem2  24806  elii1  24915  xrhmeo  24926  cnheiborlem  24934  bndth  24938  tcphcphlem1  25215  ipcnlem2  25224  cncmet  25302  trirn  25380  minveclem2  25406  minveclem4  25412  ivthlem2  25432  ovolunlem1a  25476  ovolunlem1  25477  ovolfiniun  25481  ovoliunlem1  25482  ovolicc2lem4  25500  ovolicc2lem5  25501  ovolicopnf  25504  nulmbl2  25516  ioombl1lem4  25541  ioorcl2  25552  uniioombllem3  25565  uniioombllem4  25566  uniioombllem5  25567  volcn  25586  vitalilem2  25589  vitali  25593  mbfi1fseqlem5  25699  mbfi1fseqlem6  25700  itg2splitlem  25728  itg2monolem1  25730  itg2monolem3  25732  itg2mono  25733  itg2cnlem1  25741  itgle  25790  bddmulibl  25819  bddiblnc  25822  ditgsplitlem  25840  dveflem  25959  dvlip  25973  dveq0  25980  dvfsumabs  26003  dvfsumlem1  26006  dvfsumlem2  26007  dvfsumlem3  26008  dvfsumlem4  26009  dvfsum2  26014  fta1glem2  26147  dgradd2  26246  plydiveu  26278  fta1lem  26287  aalioulem2  26313  aalioulem3  26314  aalioulem4  26315  aalioulem5  26316  aaliou3lem8  26325  aaliou3lem9  26330  ulmbdd  26379  ulmcn  26380  mtest  26385  mtestbdd  26386  abelthlem2  26413  abelthlem7  26419  pilem2  26433  tanabsge  26486  cosordlem  26510  tanord  26518  logneg2  26595  abslogle  26598  dvlog2lem  26632  cxple2a  26679  abscxpbnd  26733  atans2  26911  leibpi  26922  o1cxp  26955  cxploglim2  26959  jensenlem2  26968  emcllem6  26981  harmoniclbnd  26989  harmonicubnd  26990  harmonicbnd4  26991  fsumharmonic  26992  lgamgulmlem2  27010  lgamgulmlem3  27011  lgamgulmlem5  27013  lgambdd  27017  ftalem2  27054  basellem3  27063  basellem5  27065  basellem6  27066  dvdsflsumcom  27168  fsumfldivdiaglem  27169  ppiub  27184  chtublem  27191  logfac2  27197  chpub  27200  logfacubnd  27201  logfaclbnd  27202  logfacbnd3  27203  logexprlim  27205  bcmono  27257  bpos1lem  27262  bposlem1  27264  bposlem2  27265  bposlem3  27266  bposlem4  27267  bposlem5  27268  bposlem6  27269  bposlem7  27270  bposlem9  27272  lgsdirprm  27311  lgsquadlem1  27360  2lgslem1c  27373  2sqlem8  27406  chebbnd1lem1  27449  chebbnd1lem3  27451  chtppilimlem1  27453  chpchtlim  27459  vmadivsumb  27463  rplogsumlem1  27464  rplogsumlem2  27465  rpvmasumlem  27467  dchrisumlema  27468  dchrisumlem2  27470  dchrisumlem3  27471  dchrmusum2  27474  dchrvmasumlem2  27478  dchrvmasumlem3  27479  dchrvmasumlema  27480  dchrvmasumiflem1  27481  dchrisum0flblem1  27488  dchrisum0flblem2  27489  dchrisum0fno1  27491  dchrisum0re  27493  dchrisum0lem1b  27495  dchrisum0lem1  27496  dchrisum0lem2a  27497  dchrisum0  27500  rplogsum  27507  mudivsum  27510  mulogsumlem  27511  logdivsum  27513  mulog2sumlem1  27514  mulog2sumlem2  27515  2vmadivsumlem  27520  log2sumbnd  27524  selberglem2  27526  selbergb  27529  selberg2lem  27530  selberg2b  27532  chpdifbndlem1  27533  logdivbnd  27536  selberg3lem1  27537  selberg3lem2  27538  selberg4lem1  27540  pntrmax  27544  pntrsumo1  27545  pntrsumbnd  27546  pntrlog2bndlem1  27557  pntrlog2bndlem2  27558  pntrlog2bndlem3  27559  pntrlog2bndlem5  27561  pntrlog2bndlem6  27563  pntrlog2bnd  27564  pntpbnd1a  27565  pntpbnd1  27566  pntpbnd2  27567  pntibndlem2  27571  pntibndlem3  27572  pntlemg  27578  pntlemr  27582  pntlemj  27583  pntlemf  27585  pntlemk  27586  pntlemo  27587  pntleml  27591  abvcxp  27595  qabvle  27605  padicabv  27610  ostth2lem2  27614  ostth2lem3  27615  ostth3  27618  axlowdimlem16  29043  axcontlem8  29057  axcontlem10  29059  wwlksm1edg  29967  wwlksubclwwlk  30146  smcnlem  30786  nmoub3i  30862  ubthlem3  30961  minvecolem2  30964  minvecolem3  30965  minvecolem4  30969  htthlem  31006  bcs2  31271  pjhthlem1  31480  cnlnadjlem2  32157  cnlnadjlem7  32162  nmopadjlem  32178  nmoptrii  32183  nmopcoadji  32190  leopnmid  32227  cdj1i  32522  nndiffz1  32877  nexple  32935  oexpled  32938  pmtrto1cl  33178  psgnfzto1stlem  33179  fzto1st  33182  psgnfzto1st  33184  cyc3conja  33236  constrresqrtcl  33940  cos9thpiminplylem1  33945  smatrcl  33959  submateqlem1  33970  esumpcvgval  34241  oddpwdc  34517  eulerpartlems  34523  eulerpartlemgc  34525  eulerpartlemb  34531  dstfrvunirn  34638  orvclteinc  34639  ballotlemsima  34679  ballotlemfrcn0  34693  signstfveq0  34740  fsum2dsub  34770  breprexplemc  34795  breprexp  34796  logdivsqrle  34813  hgt750lemb  34819  hgt750leme  34821  tgoldbachgnn  34822  dnibndlem2  36758  dnibndlem6  36762  dnibndlem9  36765  dnibndlem10  36766  dnibndlem11  36767  dnibndlem12  36768  knoppcnlem4  36775  unblimceq0lem  36785  unblimceq0  36786  unbdqndv2lem2  36789  knoppndvlem11  36801  knoppndvlem14  36804  knoppndvlem15  36805  knoppndvlem18  36808  knoppndvlem21  36811  poimirlem6  37964  poimirlem7  37965  poimirlem13  37971  poimirlem15  37973  poimirlem29  37987  mblfinlem2  37996  mblfinlem3  37997  mblfinlem4  37998  ismblfin  37999  itg2addnc  38012  iblmulc2nc  38023  ftc1anclem7  38037  ftc1anclem8  38038  filbcmb  38078  geomcau  38097  prdsbnd  38131  cntotbnd  38134  bfplem2  38161  rrntotbnd  38174  iccbnd  38178  lcmineqlem20  42504  lcmineqlem21  42505  lcmineqlem22  42506  3lexlogpow5ineq2  42511  3lexlogpow5ineq5  42516  aks4d1p1p2  42526  aks4d1p1p4  42527  aks4d1p1p7  42530  aks4d1p1p5  42531  aks4d1p1  42532  aks4d1p2  42533  aks4d1p3  42534  aks4d1p5  42536  aks4d1p6  42537  aks4d1p7d1  42538  aks4d1p7  42539  aks4d1p8  42543  posbezout  42556  aks6d1c1  42572  aks6d1c2lem4  42583  2np3bcnp1  42600  sticksstones6  42607  sticksstones7  42608  sticksstones10  42611  sticksstones12a  42613  sticksstones12  42614  sticksstones22  42624  bcled  42634  bcle2d  42635  aks6d1c7lem1  42636  aks6d1c7lem2  42637  unitscyglem4  42654  lzunuz  43217  irrapxlem3  43273  irrapxlem4  43274  irrapxlem5  43275  pellexlem2  43279  pell1qrge1  43319  monotoddzzfi  43391  jm2.17a  43409  rmygeid  43413  fzmaxdif  43430  jm2.27c  43456  jm3.1lem1  43466  expdiophlem1  43470  fzunt  43903  fzuntd  43904  fzunt1d  43905  fzuntgd  43906  imo72b2lem0  44613  int-ineqtransd  44642  dvgrat  44760  monoords  45751  absnpncan2d  45756  absnpncan3d  45761  ssfiunibd  45763  rexabslelem  45867  uzublem  45879  sqrlearg  46004  fmul01  46031  fmul01lt1lem1  46035  fmul01lt1lem2  46036  climsuselem1  46058  climsuse  46059  limsupresico  46149  limsupubuzlem  46161  limsupmnfuzlem  46175  limsupre3uzlem  46184  liminfresico  46220  limsup10exlem  46221  cnrefiisplem  46278  dvdivbd  46372  dvbdfbdioolem2  46378  ioodvbdlimc1lem1  46380  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnmul  46392  dvnprodlem1  46395  dvnprodlem2  46396  iblspltprt  46422  itgspltprt  46428  stoweidlem1  46450  stoweidlem3  46452  stoweidlem5  46454  stoweidlem11  46460  stoweidlem17  46466  stoweidlem20  46469  stoweidlem26  46475  stoweidlem34  46483  wallispilem4  46517  stirlinglem11  46533  stirlinglem12  46534  stirlinglem13  46535  fourierdlem12  46568  fourierdlem15  46571  fourierdlem20  46576  fourierdlem30  46586  fourierdlem39  46595  fourierdlem42  46598  fourierdlem47  46602  fourierdlem50  46605  fourierdlem64  46619  fourierdlem65  46620  fourierdlem68  46623  fourierdlem73  46628  fourierdlem77  46632  fourierdlem79  46634  fourierdlem87  46642  elaa2lem  46682  etransclem23  46706  ioorrnopnlem  46753  salgencntex  46792  sge0le  46856  sge0isum  46876  sge0xaddlem1  46882  hoicvr  46997  hsphoidmvle2  47034  hoidmv1lelem1  47040  hoidmv1lelem2  47041  hoidmv1lelem3  47042  hoidmvlelem1  47044  hoidmvlelem2  47045  hoidmvlelem4  47047  hspmbllem1  47075  hspmbllem2  47076  smfmullem1  47240  smfmullem2  47241  smfmullem3  47242  smfsuplem1  47260  ormkglobd  47324  natglobalincr  47326  2ltceilhalf  47795  ceilhalfnn  47803  modmknepk  47831  lighneallem4a  48086  nprmdvdsfacm1lem4  48101  gpgusgralem  48547  gpgedgvtx1  48553  gpg3kgrtriexlem4  48577  gpg3kgrtriexlem6  48579  fllog2  49059  itcovalt2lem2lem1  49164