Theorem letrd 11391

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 11328	. . 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 11123   ≤ cle 11268

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 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7736  ax-resscn 11181  ax-pre-lttri 11198  ax-pre-lttrn 11199

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8696  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11269  df-mnf 11270  df-xr 11271  df-ltxr 11272  df-le 11273

This theorem is used by:  lesub3d  11856  le2addd  11857  supmul1  12208  supmul  12211  nn0negleid  12580  eluzuzle  12896  iccsplit  13538  supicc  13554  fzdisj  13606  ssfzunsnext  13624  difelfzle  13696  flwordi  13873  flleceil  13914  uzsup  13924  modltm1p1mod  13987  seqf1olem1  14105  zzlesq  14270  bernneq  14293  bernneq3  14295  discr1  14303  faclbnd  14354  faclbnd4lem1  14357  facubnd  14364  seqcoll  14529  01sqrexlem7  15335  absle  15403  releabs  15409  absrdbnd  15429  rexuzre  15440  limsupgre  15568  lo1bddrp  15612  rlimclim1  15632  rlimresb  15652  rlimrege0  15666  o1add  15701  o1sub  15703  climsqz  15728  climsqz2  15729  rlimsqzlem  15736  rlimsqz  15737  rlimsqz2  15738  rlimno1  15741  isercoll  15755  caucvgrlem  15760  iseraltlem3  15771  o1fsum  15900  cvgcmp  15903  cvgcmpce  15905  climcnds  15940  expcnv  15953  cvgrat  15972  mertenslem2  15974  fprodle  16083  eftlub  16197  rpnnen2lem12  16313  bitsfzo  16525  isprm5  16798  isprm7  16799  eulerthlem2  16873  pcmpt2  16985  pcfac  16991  prmreclem3  17010  prmreclem4  17011  prmreclem5  17012  4sqlem11  17047  vdwlem1  17073  vdwlem3  17075  setsstruct2  17266  prdsxmetlem  24594  nrmmetd  24800  nm2dif  24851  nlmvscnlem2  24911  nmoco  24963  nmotri  24965  nghmcn  24971  icccmplem2  25050  reconnlem2  25054  elii1  25163  xrhmeo  25174  cnheiborlem  25182  bndth  25186  tcphcphlem1  25463  ipcnlem2  25472  cncmet  25550  trirn  25628  minveclem2  25654  minveclem4  25660  ivthlem2  25680  ovolunlem1a  25724  ovolunlem1  25725  ovolfiniun  25729  ovoliunlem1  25730  ovolicc2lem4  25748  ovolicc2lem5  25749  ovolicopnf  25752  nulmbl2  25764  ioombl1lem4  25789  ioorcl2  25800  uniioombllem3  25813  uniioombllem4  25814  uniioombllem5  25815  volcn  25834  vitalilem2  25837  vitali  25841  mbfi1fseqlem5  25947  mbfi1fseqlem6  25948  itg2splitlem  25976  itg2monolem1  25978  itg2monolem3  25980  itg2mono  25981  itg2cnlem1  25989  itgle  26037  bddmulibl  26066  bddiblnc  26069  ditgsplitlem  26087  dveflem  26206  dvlip  26220  dveq0  26227  dvfsumabs  26250  dvfsumlem1  26253  dvfsumlem2  26254  dvfsumlem3  26255  dvfsumlem4  26256  dvfsum2  26261  fta1glem2  26394  dgradd2  26494  plydiveu  26528  fta1lem  26537  aalioulem2  26569  aalioulem3  26570  aalioulem4  26571  aalioulem5  26572  aaliou3lem8  26581  aaliou3lem9  26586  ulmbdd  26634  ulmcn  26635  mtest  26640  mtestbdd  26641  abelthlem2  26668  abelthlem7  26674  pilem2  26688  tanabsge  26744  cosordlem  26767  tanord  26775  logneg2  26852  abslogle  26855  dvlog2lem  26889  cxple2a  26936  abscxpbnd  26990  atans2  27168  leibpi  27179  o1cxp  27211  cxploglim2  27215  jensenlem2  27224  emcllem6  27237  harmoniclbnd  27245  harmonicubnd  27246  harmonicbnd4  27247  fsumharmonic  27248  lgamgulmlem2  27266  lgamgulmlem3  27267  lgamgulmlem5  27269  lgambdd  27273  ftalem2  27310  basellem3  27319  basellem5  27321  basellem6  27322  dvdsflsumcom  27424  fsumfldivdiaglem  27425  ppiub  27440  chtublem  27447  logfac2  27453  chpub  27456  logfacubnd  27457  logfaclbnd  27458  logfacbnd3  27459  logexprlim  27461  bcmono  27513  bpos1lem  27518  bposlem1  27520  bposlem2  27521  bposlem3  27522  bposlem4  27523  bposlem5  27524  bposlem6  27525  bposlem7  27526  bposlem9  27528  lgsdirprm  27567  lgsquadlem1  27616  2lgslem1c  27629  2sqlem8  27662  chebbnd1lem1  27705  chebbnd1lem3  27707  chtppilimlem1  27709  chpchtlim  27715  vmadivsumb  27719  rplogsumlem1  27720  rplogsumlem2  27721  rpvmasumlem  27723  dchrisumlema  27724  dchrisumlem2  27726  dchrisumlem3  27727  dchrmusum2  27730  dchrvmasumlem2  27734  dchrvmasumlem3  27735  dchrvmasumlema  27736  dchrvmasumiflem1  27737  dchrisum0flblem1  27744  dchrisum0flblem2  27745  dchrisum0fno1  27747  dchrisum0re  27749  dchrisum0lem1b  27751  dchrisum0lem1  27752  dchrisum0lem2a  27753  dchrisum0  27756  rplogsum  27763  mudivsum  27766  mulogsumlem  27767  logdivsum  27769  mulog2sumlem1  27770  mulog2sumlem2  27771  2vmadivsumlem  27776  log2sumbnd  27780  selberglem2  27782  selbergb  27785  selberg2lem  27786  selberg2b  27788  chpdifbndlem1  27789  logdivbnd  27792  selberg3lem1  27793  selberg3lem2  27794  selberg4lem1  27796  pntrmax  27800  pntrsumo1  27801  pntrsumbnd  27802  pntrlog2bndlem1  27813  pntrlog2bndlem2  27814  pntrlog2bndlem3  27815  pntrlog2bndlem5  27817  pntrlog2bndlem6  27819  pntrlog2bnd  27820  pntpbnd1a  27821  pntpbnd1  27822  pntpbnd2  27823  pntibndlem2  27827  pntibndlem3  27828  pntlemg  27834  pntlemr  27838  pntlemj  27839  pntlemf  27841  pntlemk  27842  pntlemo  27843  pntleml  27847  abvcxp  27851  qabvle  27861  padicabv  27866  ostth2lem2  27870  ostth2lem3  27871  ostth3  27874  axlowdimlem16  29414  axcontlem8  29428  axcontlem10  29430  wwlksm1edg  30349  wwlksubclwwlk  30528  smcnlem  31178  nmoub3i  31254  ubthlem3  31353  minvecolem2  31356  minvecolem3  31357  minvecolem4  31361  htthlem  31398  bcs2  31663  pjhthlem1  31872  cnlnadjlem2  32549  cnlnadjlem7  32554  nmopadjlem  32570  nmoptrii  32575  nmopcoadji  32582  leopnmid  32619  cdj1i  32914  nndiffz1  33257  nexple  33303  oexpled  33306  pmtrto1cl  33539  psgnfzto1stlem  33540  fzto1st  33543  psgnfzto1st  33545  cyc3conja  33597  constrresqrtcl  34287  cos9thpiminplylem1  34292  smatrcl  34306  submateqlem1  34317  esumpcvgval  34588  oddpwdc  34865  eulerpartlems  34871  eulerpartlemgc  34873  eulerpartlemb  34879  dstfrvunirn  34986  orvclteinc  34987  ballotlemsima  35027  ballotlemfrcn0  35041  signstfveq0  35085  fsum2dsub  35115  breprexplemc  35140  breprexp  35141  logdivsqrle  35158  hgt750lemb  35164  hgt750leme  35166  tgoldbachgnn  35167  dnibndlem2  37176  dnibndlem6  37180  dnibndlem9  37183  dnibndlem10  37184  dnibndlem11  37185  dnibndlem12  37186  knoppcnlem4  37193  unblimceq0lem  37203  unblimceq0  37204  unbdqndv2lem2  37207  knoppndvlem11  37219  knoppndvlem14  37222  knoppndvlem15  37223  knoppndvlem18  37226  knoppndvlem21  37229  poimirlem6  38375  poimirlem7  38376  poimirlem13  38382  poimirlem15  38384  poimirlem29  38398  mblfinlem2  38407  mblfinlem3  38408  mblfinlem4  38409  ismblfin  38410  itg2addnc  38423  iblmulc2nc  38434  ftc1anclem7  38448  ftc1anclem8  38449  filbcmb  38490  geomcau  38509  prdsbnd  38543  cntotbnd  38546  bfplem2  38573  rrntotbnd  38586  iccbnd  38590  lcmineqlem20  42914  lcmineqlem21  42915  lcmineqlem22  42916  3lexlogpow5ineq2  42921  3lexlogpow5ineq5  42926  aks4d1p1p2  42936  aks4d1p1p4  42937  aks4d1p1p7  42940  aks4d1p1p5  42941  aks4d1p1  42942  aks4d1p2  42943  aks4d1p3  42944  aks4d1p5  42946  aks4d1p6  42947  aks4d1p7d1  42948  aks4d1p7  42949  aks4d1p8  42953  posbezout  42966  aks6d1c1  42982  aks6d1c2lem4  42993  2np3bcnp1  43010  sticksstones6  43017  sticksstones7  43018  sticksstones10  43021  sticksstones12a  43023  sticksstones12  43024  sticksstones22  43034  bcled  43044  bcle2d  43045  aks6d1c7lem1  43046  aks6d1c7lem2  43047  unitscyglem4  43064  lzunuz  43613  irrapxlem3  43665  irrapxlem4  43666  irrapxlem5  43667  pellexlem2  43671  pell1qrge1  43711  monotoddzzfi  43783  jm2.17a  43801  rmygeid  43805  fzmaxdif  43822  jm2.27c  43848  jm3.1lem1  43858  expdiophlem1  43862  fzunt  44295  fzuntd  44296  fzunt1d  44297  fzuntgd  44298  imo72b2lem0  45005  int-ineqtransd  45034  dvgrat  45136  monoords  46130  absnpncan2d  46135  absnpncan3d  46140  ssfiunibd  46142  rexabslelem  46246  uzublem  46258  sqrlearg  46383  fmul01  46410  fmul01lt1lem1  46414  fmul01lt1lem2  46415  climsuselem1  46437  climsuse  46438  limsupresico  46528  limsupubuzlem  46540  limsupmnfuzlem  46554  limsupre3uzlem  46563  liminfresico  46599  limsup10exlem  46600  cnrefiisplem  46657  dvdivbd  46751  dvbdfbdioolem2  46757  ioodvbdlimc1lem1  46759  ioodvbdlimc1lem2  46760  ioodvbdlimc2lem  46762  dvnmul  46771  dvnprodlem1  46774  dvnprodlem2  46775  iblspltprt  46801  itgspltprt  46807  stoweidlem1  46829  stoweidlem3  46831  stoweidlem5  46833  stoweidlem11  46839  stoweidlem17  46845  stoweidlem20  46848  stoweidlem26  46854  stoweidlem34  46862  wallispilem4  46896  stirlinglem11  46912  stirlinglem12  46913  stirlinglem13  46914  fourierdlem12  46947  fourierdlem15  46950  fourierdlem20  46955  fourierdlem30  46965  fourierdlem39  46974  fourierdlem42  46977  fourierdlem47  46981  fourierdlem50  46984  fourierdlem64  46998  fourierdlem65  46999  fourierdlem68  47002  fourierdlem73  47007  fourierdlem77  47011  fourierdlem79  47013  fourierdlem87  47021  elaa2lem  47061  etransclem23  47085  ioorrnopnlem  47132  salgencntex  47171  sge0le  47235  sge0isum  47255  sge0xaddlem1  47261  hoicvr  47376  hsphoidmvle2  47413  hoidmv1lelem1  47419  hoidmv1lelem2  47420  hoidmv1lelem3  47421  hoidmvlelem1  47423  hoidmvlelem2  47424  hoidmvlelem4  47426  hspmbllem1  47454  hspmbllem2  47455  smfmullem1  47619  smfmullem2  47620  smfmullem3  47621  smfsuplem1  47639  ormkglobd  47705  2ltceilhalf  48220  ceilhalfnn  48228  modmknepk  48256  lighneallem4a  48511  nprmdvdsfacm1lem4  48526  gpgusgralem  48972  gpgedgvtx1  48978  gpg3kgrtriexlem4  49002  gpg3kgrtriexlem6  49004  fllog2  49498  itcovalt2lem2lem1  49603