Theorem letrd 11362

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   class class class wbr 5109  ℝcr 11094   ≤ cle 11239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-pre-lttri 11169  ax-pre-lttrn 11170

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244

This theorem is referenced by:  lesub3d  11827  le2addd  11828  supmul1  12179  supmul  12182  nn0negleid  12551  eluzuzle  12866  iccsplit  13507  supicc  13523  fzdisj  13575  ssfzunsnext  13593  difelfzle  13665  flwordi  13841  flleceil  13882  uzsup  13892  modltm1p1mod  13955  seqf1olem1  14073  zzlesq  14238  bernneq  14261  bernneq3  14263  discr1  14271  faclbnd  14322  faclbnd4lem1  14325  facubnd  14332  seqcoll  14497  01sqrexlem7  15295  absle  15363  releabs  15369  absrdbnd  15389  rexuzre  15400  limsupgre  15528  lo1bddrp  15572  rlimclim1  15592  rlimresb  15612  rlimrege0  15626  o1add  15661  o1sub  15663  climsqz  15688  climsqz2  15689  rlimsqzlem  15696  rlimsqz  15697  rlimsqz2  15698  rlimno1  15701  isercoll  15715  caucvgrlem  15720  iseraltlem3  15731  o1fsum  15861  cvgcmp  15864  cvgcmpce  15866  climcnds  15901  expcnv  15914  cvgrat  15933  mertenslem2  15935  fprodle  16046  eftlub  16160  rpnnen2lem12  16276  bitsfzo  16488  isprm5  16761  isprm7  16762  eulerthlem2  16836  pcmpt2  16948  pcfac  16954  prmreclem3  16973  prmreclem4  16974  prmreclem5  16975  4sqlem11  17010  vdwlem1  17036  vdwlem3  17038  setsstruct2  17229  prdsxmetlem  24525  nrmmetd  24731  nm2dif  24782  nlmvscnlem2  24842  nmoco  24894  nmotri  24896  nghmcn  24902  icccmplem2  24981  reconnlem2  24985  elii1  25094  xrhmeo  25105  cnheiborlem  25113  bndth  25117  tcphcphlem1  25394  ipcnlem2  25403  cncmet  25481  trirn  25559  minveclem2  25585  minveclem4  25591  ivthlem2  25611  ovolunlem1a  25655  ovolunlem1  25656  ovolfiniun  25660  ovoliunlem1  25661  ovolicc2lem4  25679  ovolicc2lem5  25680  ovolicopnf  25683  nulmbl2  25695  ioombl1lem4  25720  ioorcl2  25731  uniioombllem3  25744  uniioombllem4  25745  uniioombllem5  25746  volcn  25765  vitalilem2  25768  vitali  25772  mbfi1fseqlem5  25878  mbfi1fseqlem6  25879  itg2splitlem  25907  itg2monolem1  25909  itg2monolem3  25911  itg2mono  25912  itg2cnlem1  25920  itgle  25969  bddmulibl  25998  bddiblnc  26001  ditgsplitlem  26019  dveflem  26138  dvlip  26152  dveq0  26159  dvfsumabs  26182  dvfsumlem1  26185  dvfsumlem2  26186  dvfsumlem3  26187  dvfsumlem4  26188  dvfsum2  26193  fta1glem2  26326  dgradd2  26425  plydiveu  26459  fta1lem  26468  aalioulem2  26496  aalioulem3  26497  aalioulem4  26498  aalioulem5  26499  aaliou3lem8  26508  aaliou3lem9  26513  ulmbdd  26561  ulmcn  26562  mtest  26567  mtestbdd  26568  abelthlem2  26595  abelthlem7  26601  pilem2  26615  tanabsge  26671  cosordlem  26695  tanord  26703  logneg2  26780  abslogle  26783  dvlog2lem  26817  cxple2a  26864  abscxpbnd  26918  atans2  27096  leibpi  27107  o1cxp  27139  cxploglim2  27143  jensenlem2  27152  emcllem6  27165  harmoniclbnd  27173  harmonicubnd  27174  harmonicbnd4  27175  fsumharmonic  27176  lgamgulmlem2  27194  lgamgulmlem3  27195  lgamgulmlem5  27197  lgambdd  27201  ftalem2  27238  basellem3  27247  basellem5  27249  basellem6  27250  dvdsflsumcom  27352  fsumfldivdiaglem  27353  ppiub  27368  chtublem  27375  logfac2  27381  chpub  27384  logfacubnd  27385  logfaclbnd  27386  logfacbnd3  27387  logexprlim  27389  bcmono  27441  bpos1lem  27446  bposlem1  27448  bposlem2  27449  bposlem3  27450  bposlem4  27451  bposlem5  27452  bposlem6  27453  bposlem7  27454  bposlem9  27456  lgsdirprm  27495  lgsquadlem1  27544  2lgslem1c  27557  2sqlem8  27590  chebbnd1lem1  27633  chebbnd1lem3  27635  chtppilimlem1  27637  chpchtlim  27643  vmadivsumb  27647  rplogsumlem1  27648  rplogsumlem2  27649  rpvmasumlem  27651  dchrisumlema  27652  dchrisumlem2  27654  dchrisumlem3  27655  dchrmusum2  27658  dchrvmasumlem2  27662  dchrvmasumlem3  27663  dchrvmasumlema  27664  dchrvmasumiflem1  27665  dchrisum0flblem1  27672  dchrisum0flblem2  27673  dchrisum0fno1  27675  dchrisum0re  27677  dchrisum0lem1b  27679  dchrisum0lem1  27680  dchrisum0lem2a  27681  dchrisum0  27684  rplogsum  27691  mudivsum  27694  mulogsumlem  27695  logdivsum  27697  mulog2sumlem1  27698  mulog2sumlem2  27699  2vmadivsumlem  27704  log2sumbnd  27708  selberglem2  27710  selbergb  27713  selberg2lem  27714  selberg2b  27716  chpdifbndlem1  27717  logdivbnd  27720  selberg3lem1  27721  selberg3lem2  27722  selberg4lem1  27724  pntrmax  27728  pntrsumo1  27729  pntrsumbnd  27730  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem5  27745  pntrlog2bndlem6  27747  pntrlog2bnd  27748  pntpbnd1a  27749  pntpbnd1  27750  pntpbnd2  27751  pntibndlem2  27755  pntibndlem3  27756  pntlemg  27762  pntlemr  27766  pntlemj  27767  pntlemf  27769  pntlemk  27770  pntlemo  27771  pntleml  27775  abvcxp  27779  qabvle  27789  padicabv  27794  ostth2lem2  27798  ostth2lem3  27799  ostth3  27802  axlowdimlem16  29307  axcontlem8  29321  axcontlem10  29323  wwlksm1edg  30230  wwlksubclwwlk  30409  smcnlem  31049  nmoub3i  31125  ubthlem3  31224  minvecolem2  31227  minvecolem3  31228  minvecolem4  31232  htthlem  31269  bcs2  31534  pjhthlem1  31743  cnlnadjlem2  32420  cnlnadjlem7  32425  nmopadjlem  32441  nmoptrii  32446  nmopcoadji  32453  leopnmid  32490  cdj1i  32785  nndiffz1  33131  nexple  33177  oexpled  33180  pmtrto1cl  33419  psgnfzto1stlem  33420  fzto1st  33423  psgnfzto1st  33425  cyc3conja  33477  constrresqrtcl  34167  cos9thpiminplylem1  34172  smatrcl  34186  submateqlem1  34197  esumpcvgval  34468  oddpwdc  34744  eulerpartlems  34750  eulerpartlemgc  34752  eulerpartlemb  34758  dstfrvunirn  34865  orvclteinc  34866  ballotlemsima  34906  ballotlemfrcn0  34920  signstfveq0  34964  fsum2dsub  34994  breprexplemc  35019  breprexp  35020  logdivsqrle  35037  hgt750lemb  35043  hgt750leme  35045  tgoldbachgnn  35046  dnibndlem2  37068  dnibndlem6  37072  dnibndlem9  37075  dnibndlem10  37076  dnibndlem11  37077  dnibndlem12  37078  knoppcnlem4  37085  unblimceq0lem  37095  unblimceq0  37096  unbdqndv2lem2  37099  knoppndvlem11  37111  knoppndvlem14  37114  knoppndvlem15  37115  knoppndvlem18  37118  knoppndvlem21  37121  poimirlem6  38277  poimirlem7  38278  poimirlem13  38284  poimirlem15  38286  poimirlem29  38300  mblfinlem2  38309  mblfinlem3  38310  mblfinlem4  38311  ismblfin  38312  itg2addnc  38325  iblmulc2nc  38336  ftc1anclem7  38350  ftc1anclem8  38351  filbcmb  38391  geomcau  38410  prdsbnd  38444  cntotbnd  38447  bfplem2  38474  rrntotbnd  38487  iccbnd  38491  lcmineqlem20  42815  lcmineqlem21  42816  lcmineqlem22  42817  3lexlogpow5ineq2  42822  3lexlogpow5ineq5  42827  aks4d1p1p2  42837  aks4d1p1p4  42838  aks4d1p1p7  42841  aks4d1p1p5  42842  aks4d1p1  42843  aks4d1p2  42844  aks4d1p3  42845  aks4d1p5  42847  aks4d1p6  42848  aks4d1p7d1  42849  aks4d1p7  42850  aks4d1p8  42854  posbezout  42867  aks6d1c1  42883  aks6d1c2lem4  42894  2np3bcnp1  42911  sticksstones6  42918  sticksstones7  42919  sticksstones10  42922  sticksstones12a  42924  sticksstones12  42925  sticksstones22  42935  bcled  42945  bcle2d  42946  aks6d1c7lem1  42947  aks6d1c7lem2  42948  unitscyglem4  42965  lzunuz  43499  irrapxlem3  43551  irrapxlem4  43552  irrapxlem5  43553  pellexlem2  43557  pell1qrge1  43597  monotoddzzfi  43669  jm2.17a  43687  rmygeid  43691  fzmaxdif  43708  jm2.27c  43734  jm3.1lem1  43744  expdiophlem1  43748  fzunt  44181  fzuntd  44182  fzunt1d  44183  fzuntgd  44184  imo72b2lem0  44891  int-ineqtransd  44920  dvgrat  45022  monoords  46016  absnpncan2d  46021  absnpncan3d  46026  ssfiunibd  46028  rexabslelem  46132  uzublem  46144  sqrlearg  46269  fmul01  46296  fmul01lt1lem1  46300  fmul01lt1lem2  46301  climsuselem1  46323  climsuse  46324  limsupresico  46414  limsupubuzlem  46426  limsupmnfuzlem  46440  limsupre3uzlem  46449  liminfresico  46485  limsup10exlem  46486  cnrefiisplem  46543  dvdivbd  46637  dvbdfbdioolem2  46643  ioodvbdlimc1lem1  46645  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  dvnmul  46657  dvnprodlem1  46660  dvnprodlem2  46661  iblspltprt  46687  itgspltprt  46693  stoweidlem1  46715  stoweidlem3  46717  stoweidlem5  46719  stoweidlem11  46725  stoweidlem17  46731  stoweidlem20  46734  stoweidlem26  46740  stoweidlem34  46748  wallispilem4  46782  stirlinglem11  46798  stirlinglem12  46799  stirlinglem13  46800  fourierdlem12  46833  fourierdlem15  46836  fourierdlem20  46841  fourierdlem30  46851  fourierdlem39  46860  fourierdlem42  46863  fourierdlem47  46867  fourierdlem50  46870  fourierdlem64  46884  fourierdlem65  46885  fourierdlem68  46888  fourierdlem73  46893  fourierdlem77  46897  fourierdlem79  46899  fourierdlem87  46907  elaa2lem  46947  etransclem23  46971  ioorrnopnlem  47018  salgencntex  47057  sge0le  47121  sge0isum  47141  sge0xaddlem1  47147  hoicvr  47262  hsphoidmvle2  47299  hoidmv1lelem1  47305  hoidmv1lelem2  47306  hoidmv1lelem3  47307  hoidmvlelem1  47309  hoidmvlelem2  47310  hoidmvlelem4  47312  hspmbllem1  47340  hspmbllem2  47341  smfmullem1  47505  smfmullem2  47506  smfmullem3  47507  smfsuplem1  47525  ormkglobd  47591  natglobalincr  47593  2ltceilhalf  48069  ceilhalfnn  48077  modmknepk  48105  lighneallem4a  48360  nprmdvdsfacm1lem4  48375  gpgusgralem  48821  gpgedgvtx1  48827  gpg3kgrtriexlem4  48851  gpg3kgrtriexlem6  48853  fllog2  49348  itcovalt2lem2lem1  49453