Theorem letrd 11460

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   class class class wbr 5103  ℝcr 11192   ≤ cle 11337

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7749  ax-resscn 11250  ax-pre-lttri 11267  ax-pre-lttrn 11268

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 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3063  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-er 8710  df-en 8967  df-dom 8968  df-sdom 8969  df-pnf 11338  df-mnf 11339  df-xr 11340  df-ltxr 11341  df-le 11342

This theorem is used by:  lesub3d  11927  le2addd  11928  supmul1  12279  supmul  12282  nn0negleid  12651  eluzuzle  12967  iccsplit  13609  supicc  13625  fzdisj  13678  ssfzunsnext  13696  difelfzle  13768  flwordi  13945  flleceil  13986  uzsup  13996  modltm1p1mod  14059  seqf1olem1  14177  zzlesq  14343  bernneq  14366  bernneq3  14368  discr1  14376  faclbnd  14427  faclbnd4lem1  14430  facubnd  14437  seqcoll  14602  01sqrexlem7  15408  absle  15476  releabs  15482  absrdbnd  15502  rexuzre  15513  limsupgre  15641  lo1bddrp  15685  rlimclim1  15705  rlimresb  15725  rlimrege0  15739  o1add  15774  o1sub  15776  climsqz  15801  climsqz2  15802  rlimsqzlem  15809  rlimsqz  15810  rlimsqz2  15811  rlimno1  15814  isercoll  15828  caucvgrlem  15833  iseraltlem3  15844  o1fsum  15973  cvgcmp  15976  cvgcmpce  15978  climcnds  16013  expcnv  16026  cvgrat  16045  mertenslem2  16047  fprodle  16156  eftlub  16270  rpnnen2lem12  16386  bitsfzo  16598  isprm5  16876  isprm7  16877  eulerthlem2  16952  pcmpt2  17064  pcfac  17070  prmreclem3  17089  prmreclem4  17090  prmreclem5  17091  4sqlem11  17126  vdwlem1  17152  vdwlem3  17154  setsstruct2  17345  prdsxmetlem  24680  nrmmetd  24886  nm2dif  24937  nlmvscnlem2  24997  nmoco  25049  nmotri  25051  nghmcn  25057  icccmplem2  25136  reconnlem2  25140  elii1  25249  xrhmeo  25260  cnheiborlem  25268  bndth  25272  tcphcphlem1  25549  ipcnlem2  25558  cncmet  25636  trirn  25714  minveclem2  25740  minveclem4  25746  ivthlem2  25766  ovolunlem1a  25810  ovolunlem1  25811  ovolfiniun  25815  ovoliunlem1  25816  ovolicc2lem4  25834  ovolicc2lem5  25835  ovolicopnf  25838  nulmbl2  25850  ioombl1lem4  25875  ioorcl2  25886  uniioombllem3  25899  uniioombllem4  25900  uniioombllem5  25901  volcn  25920  vitalilem2  25923  vitali  25927  mbfi1fseqlem5  26033  mbfi1fseqlem6  26034  itg2splitlem  26062  itg2monolem1  26064  itg2monolem3  26066  itg2mono  26067  itg2cnlem1  26075  itgle  26123  bddmulibl  26152  bddiblnc  26155  ditgsplitlem  26173  dveflem  26292  dvlip  26306  dveq0  26313  dvfsumabs  26336  dvfsumlem1  26339  dvfsumlem2  26340  dvfsumlem3  26341  dvfsumlem4  26342  dvfsum2  26347  fta1glem2  26480  dgradd2  26580  plydiveu  26612  fta1lem  26621  aalioulem2  26653  aalioulem3  26654  aalioulem4  26655  aalioulem5  26656  aaliou3lem8  26665  aaliou3lem9  26670  ulmbdd  26718  ulmcn  26719  mtest  26724  mtestbdd  26725  abelthlem2  26752  abelthlem7  26758  pilem2  26772  tanabsge  26828  cosordlem  26851  tanord  26859  logneg2  26936  abslogle  26939  dvlog2lem  26973  cxple2a  27020  abscxpbnd  27074  atans2  27252  leibpi  27263  o1cxp  27295  cxploglim2  27299  jensenlem2  27308  emcllem6  27321  harmoniclbnd  27329  harmonicubnd  27330  harmonicbnd4  27331  fsumharmonic  27332  lgamgulmlem2  27350  lgamgulmlem3  27351  lgamgulmlem5  27353  lgambdd  27357  ftalem2  27394  basellem3  27403  basellem5  27405  basellem6  27406  dvdsflsumcom  27508  fsumfldivdiaglem  27509  ppiub  27524  chtublem  27531  logfac2  27537  chpub  27540  logfacubnd  27541  logfaclbnd  27542  logfacbnd3  27543  logexprlim  27545  bcmono  27597  bpos1lem  27602  bposlem1  27604  bposlem2  27605  bposlem3  27606  bposlem4  27607  bposlem5  27608  bposlem6  27609  bposlem7  27610  bposlem9  27612  lgsdirprm  27651  lgsquadlem1  27700  2lgslem1c  27713  2sqlem8  27746  chebbnd1lem1  27789  chebbnd1lem3  27791  chtppilimlem1  27793  chpchtlim  27799  vmadivsumb  27803  rplogsumlem1  27804  rplogsumlem2  27805  rpvmasumlem  27807  dchrisumlema  27808  dchrisumlem2  27810  dchrisumlem3  27811  dchrmusum2  27814  dchrvmasumlem2  27818  dchrvmasumlem3  27819  dchrvmasumlema  27820  dchrvmasumiflem1  27821  dchrisum0flblem1  27828  dchrisum0flblem2  27829  dchrisum0fno1  27831  dchrisum0re  27833  dchrisum0lem1b  27835  dchrisum0lem1  27836  dchrisum0lem2a  27837  dchrisum0  27840  rplogsum  27847  mudivsum  27850  mulogsumlem  27851  logdivsum  27853  mulog2sumlem1  27854  mulog2sumlem2  27855  2vmadivsumlem  27860  log2sumbnd  27864  selberglem2  27866  selbergb  27869  selberg2lem  27870  selberg2b  27872  chpdifbndlem1  27873  logdivbnd  27876  selberg3lem1  27877  selberg3lem2  27878  selberg4lem1  27880  pntrmax  27884  pntrsumo1  27885  pntrsumbnd  27886  pntrlog2bndlem1  27897  pntrlog2bndlem2  27898  pntrlog2bndlem3  27899  pntrlog2bndlem5  27901  pntrlog2bndlem6  27903  pntrlog2bnd  27904  pntpbnd1a  27905  pntpbnd1  27906  pntpbnd2  27907  pntibndlem2  27911  pntibndlem3  27912  pntlemg  27918  pntlemr  27922  pntlemj  27923  pntlemf  27925  pntlemk  27926  pntlemo  27927  pntleml  27931  abvcxp  27935  qabvle  27945  padicabv  27950  ostth2lem2  27954  ostth2lem3  27955  ostth3  27958  axlowdimlem16  29528  axcontlem8  29542  axcontlem10  29544  wwlksm1edg  30463  wwlksubclwwlk  30642  smcnlem  31292  nmoub3i  31368  ubthlem3  31467  minvecolem2  31470  minvecolem3  31471  minvecolem4  31475  htthlem  31512  bcs2  31777  pjhthlem1  31986  cnlnadjlem2  32663  cnlnadjlem7  32668  nmopadjlem  32684  nmoptrii  32689  nmopcoadji  32696  leopnmid  32733  cdj1i  33028  nndiffz1  33371  nexple  33417  oexpled  33420  pmtrto1cl  33653  psgnfzto1stlem  33654  fzto1st  33657  psgnfzto1st  33659  cyc3conja  33711  constrresqrtcl  34402  cos9thpiminplylem1  34407  smatrcl  34421  submateqlem1  34432  esumpcvgval  34703  oddpwdc  34979  eulerpartlems  34985  eulerpartlemgc  34987  eulerpartlemb  34993  dstfrvunirn  35100  orvclteinc  35101  ballotlemsima  35141  ballotlemfrcn0  35155  signstfveq0  35199  fsum2dsub  35229  breprexplemc  35254  breprexp  35255  logdivsqrle  35272  hgt750lemb  35278  hgt750leme  35280  tgoldbachgnn  35281  dnibndlem2  37325  dnibndlem6  37329  dnibndlem9  37332  dnibndlem10  37333  dnibndlem11  37334  dnibndlem12  37335  knoppcnlem4  37342  unblimceq0lem  37352  unblimceq0  37353  unbdqndv2lem2  37356  knoppndvlem11  37368  knoppndvlem14  37371  knoppndvlem15  37372  knoppndvlem18  37375  knoppndvlem21  37378  poimirlem6  38524  poimirlem7  38525  poimirlem13  38531  poimirlem15  38533  poimirlem29  38547  mblfinlem2  38556  mblfinlem3  38557  mblfinlem4  38558  ismblfin  38559  itg2addnc  38572  iblmulc2nc  38583  ftc1anclem7  38597  ftc1anclem8  38598  filbcmb  38654  geomcau  38673  prdsbnd  38707  cntotbnd  38710  bfplem2  38737  rrntotbnd  38750  iccbnd  38754  lcmineqlem20  43078  lcmineqlem21  43079  lcmineqlem22  43080  3lexlogpow5ineq2  43085  3lexlogpow5ineq5  43090  aks4d1p1p2  43100  aks4d1p1p4  43101  aks4d1p1p7  43104  aks4d1p1p5  43105  aks4d1p1  43106  aks4d1p2  43107  aks4d1p3  43108  aks4d1p5  43110  aks4d1p6  43111  aks4d1p7d1  43112  aks4d1p7  43113  aks4d1p8  43117  posbezout  43130  aks6d1c1  43146  aks6d1c2lem4  43157  2np3bcnp1  43174  sticksstones6  43181  sticksstones7  43182  sticksstones10  43185  sticksstones12a  43187  sticksstones12  43188  sticksstones22  43198  bcled  43208  bcle2d  43209  aks6d1c7lem1  43210  aks6d1c7lem2  43211  unitscyglem4  43228  lzunuz  43758  irrapxlem3  43810  irrapxlem4  43811  irrapxlem5  43812  pellexlem2  43816  pell1qrge1  43856  monotoddzzfi  43928  jm2.17a  43946  rmygeid  43950  fzmaxdif  43967  jm2.27c  43993  jm3.1lem1  44003  expdiophlem1  44007  fzunt  44440  fzuntd  44441  fzunt1d  44442  fzuntgd  44443  imo72b2lem0  45150  int-ineqtransd  45179  dvgrat  45281  monoords  46282  absnpncan2d  46287  absnpncan3d  46292  ssfiunibd  46294  rexabslelem  46397  uzublem  46409  sqrlearg  46534  fmul01  46561  fmul01lt1lem1  46565  fmul01lt1lem2  46566  climsuselem1  46588  climsuse  46589  limsupresico  46679  limsupubuzlem  46691  limsupmnfuzlem  46705  limsupre3uzlem  46714  liminfresico  46750  limsup10exlem  46751  cnrefiisplem  46808  dvdivbd  46902  dvbdfbdioolem2  46908  ioodvbdlimc1lem1  46910  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnmul  46922  dvnprodlem1  46925  dvnprodlem2  46926  iblspltprt  46952  itgspltprt  46958  stoweidlem1  46980  stoweidlem3  46982  stoweidlem5  46984  stoweidlem11  46990  stoweidlem17  46996  stoweidlem20  46999  stoweidlem26  47005  stoweidlem34  47013  wallispilem4  47047  stirlinglem11  47063  stirlinglem12  47064  stirlinglem13  47065  fourierdlem12  47098  fourierdlem15  47101  fourierdlem20  47106  fourierdlem30  47116  fourierdlem39  47125  fourierdlem42  47128  fourierdlem47  47132  fourierdlem50  47135  fourierdlem64  47149  fourierdlem65  47150  fourierdlem68  47153  fourierdlem73  47158  fourierdlem77  47162  fourierdlem79  47164  fourierdlem87  47172  elaa2lem  47212  etransclem23  47236  ioorrnopnlem  47283  salgencntex  47322  sge0le  47386  sge0isum  47406  sge0xaddlem1  47412  hoicvr  47527  hsphoidmvle2  47564  hoidmv1lelem1  47570  hoidmv1lelem2  47571  hoidmv1lelem3  47572  hoidmvlelem1  47574  hoidmvlelem2  47575  hoidmvlelem4  47577  hspmbllem1  47605  hspmbllem2  47606  smfmullem1  47770  smfmullem2  47771  smfmullem3  47772  smfsuplem1  47790  ormkglobd  47856  2ltceilhalf  48371  ceilhalfnn  48379  modmknepk  48407  lighneallem4a  48662  nprmdvdsfacm1lem4  48677  gpgusgralem  49123  gpgedgvtx1  49129  gpg3kgrtriexlem4  49153  gpg3kgrtriexlem6  49155  fllog2  49649  itcovalt2lem2lem1  49754