Theorem letrd 10475

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

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 2156   class class class wbr 4844  ℝcr 10216   ≤ cle 10356

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-resscn 10274  ax-pre-lttri 10291  ax-pre-lttrn 10292

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-op 4377  df-uni 4631  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5219  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-er 7975  df-en 8189  df-dom 8190  df-sdom 8191  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361

This theorem is referenced by:  lesub3d  10926  supmul1  11273  supmul  11276  nn0negleid  11607  eluzuzle  11909  iccsplit  12524  supicc  12539  fzdisj  12587  ssfzunsnext  12605  difelfzle  12672  flwordi  12833  flleceil  12872  uzsup  12882  modltm1p1mod  12942  seqf1olem1  13059  bernneq  13209  bernneq3  13211  discr1  13219  faclbnd  13293  faclbnd4lem1  13296  facubnd  13303  seqcoll  13461  sqrlem7  14208  absle  14274  releabs  14280  absrdbnd  14300  rexuzre  14311  limsupgre  14431  lo1bddrp  14475  rlimclim1  14495  rlimresb  14515  rlimrege0  14529  o1add  14563  o1sub  14565  climsqz  14590  climsqz2  14591  rlimsqzlem  14598  rlimsqz  14599  rlimsqz2  14600  rlimno1  14603  isercoll  14617  caucvgrlem  14622  iseraltlem3  14633  o1fsum  14763  cvgcmp  14766  cvgcmpce  14768  climcnds  14801  expcnv  14814  cvgrat  14832  mertenslem2  14834  fprodle  14943  eftlub  15055  rpnnen2lem12  15170  bitsfzo  15372  isprm5  15632  isprm7  15633  eulerthlem2  15700  pcmpt2  15810  pcfac  15816  prmreclem3  15835  prmreclem4  15836  prmreclem5  15837  4sqlem11  15872  vdwlem1  15898  vdwlem3  15900  setsstruct2  16103  prdsxmetlem  22383  nrmmetd  22589  nm2dif  22639  nlmvscnlem2  22699  nmoco  22751  nmotri  22753  nghmcn  22759  icccmplem2  22836  reconnlem2  22840  elii1  22944  xrhmeo  22955  cnheiborlem  22963  bndth  22967  tchcphlem1  23243  ipcnlem2  23252  cncmet  23329  trirn  23394  minveclem2  23408  minveclem4  23414  ivthlem2  23432  ovolunlem1a  23476  ovolunlem1  23477  ovolfiniun  23481  ovoliunlem1  23482  ovolicc2lem4  23500  ovolicc2lem5  23501  ovolicopnf  23504  nulmbl2  23516  ioombl1lem4  23541  ioorcl2  23552  uniioombllem3  23565  uniioombllem4  23566  uniioombllem5  23567  volcn  23586  vitalilem2  23589  vitali  23593  mbfi1fseqlem5  23699  mbfi1fseqlem6  23700  itg2splitlem  23728  itg2monolem1  23730  itg2monolem3  23732  itg2mono  23733  itg2cnlem1  23741  itgle  23789  bddmulibl  23818  ditgsplitlem  23837  dveflem  23955  dvlip  23969  dveq0  23976  dvfsumabs  23999  dvfsumlem1  24002  dvfsumlem2  24003  dvfsumlem3  24004  dvfsumlem4  24005  dvfsum2  24010  fta1glem2  24139  dgradd2  24237  plydiveu  24266  fta1lem  24275  aalioulem2  24301  aalioulem3  24302  aalioulem4  24303  aalioulem5  24304  aaliou3lem8  24313  aaliou3lem9  24318  ulmbdd  24365  ulmcn  24366  mtest  24371  mtestbdd  24372  abelthlem2  24399  abelthlem7  24405  pilem2  24419  tanabsge  24472  cosordlem  24491  tanord  24498  logneg2  24574  abslogle  24577  dvlog2lem  24611  cxple2a  24658  abscxpbnd  24707  atans2  24871  leibpi  24882  o1cxp  24914  cxploglim2  24918  jensenlem2  24927  emcllem6  24940  harmoniclbnd  24948  harmonicubnd  24949  harmonicbnd4  24950  fsumharmonic  24951  lgamgulmlem2  24969  lgamgulmlem3  24970  lgamgulmlem5  24972  lgambdd  24976  ftalem2  25013  basellem3  25022  basellem5  25024  basellem6  25025  dvdsflsumcom  25127  fsumfldivdiaglem  25128  ppiub  25142  chtublem  25149  logfac2  25155  chpub  25158  logfacubnd  25159  logfaclbnd  25160  logfacbnd3  25161  logexprlim  25163  bcmono  25215  bpos1lem  25220  bposlem1  25222  bposlem2  25223  bposlem3  25224  bposlem4  25225  bposlem5  25226  bposlem6  25227  bposlem7  25228  bposlem9  25230  lgsdirprm  25269  lgsquadlem1  25318  2lgslem1c  25331  2sqlem8  25364  chebbnd1lem1  25371  chebbnd1lem3  25373  chtppilimlem1  25375  chpchtlim  25381  vmadivsumb  25385  rplogsumlem1  25386  rplogsumlem2  25387  rpvmasumlem  25389  dchrisumlema  25390  dchrisumlem2  25392  dchrisumlem3  25393  dchrmusum2  25396  dchrvmasumlem2  25400  dchrvmasumlem3  25401  dchrvmasumlema  25402  dchrvmasumiflem1  25403  dchrisum0flblem1  25410  dchrisum0flblem2  25411  dchrisum0fno1  25413  dchrisum0re  25415  dchrisum0lem1b  25417  dchrisum0lem1  25418  dchrisum0lem2a  25419  dchrisum0  25422  rplogsum  25429  mudivsum  25432  mulogsumlem  25433  logdivsum  25435  mulog2sumlem1  25436  mulog2sumlem2  25437  2vmadivsumlem  25442  log2sumbnd  25446  selberglem2  25448  selbergb  25451  selberg2lem  25452  selberg2b  25454  chpdifbndlem1  25455  logdivbnd  25458  selberg3lem1  25459  selberg3lem2  25460  selberg4lem1  25462  pntrmax  25466  pntrsumo1  25467  pntrsumbnd  25468  pntrlog2bndlem1  25479  pntrlog2bndlem2  25480  pntrlog2bndlem3  25481  pntrlog2bndlem5  25483  pntrlog2bndlem6  25485  pntrlog2bnd  25486  pntpbnd1a  25487  pntpbnd1  25488  pntpbnd2  25489  pntibndlem2  25493  pntibndlem3  25494  pntlemg  25500  pntlemr  25504  pntlemj  25505  pntlemf  25507  pntlemk  25508  pntlemo  25509  pntleml  25513  abvcxp  25517  qabvle  25527  padicabv  25532  ostth2lem2  25536  ostth2lem3  25537  ostth3  25540  axlowdimlem16  26050  axcontlem8  26064  axcontlem10  26066  wwlksm1edg  27007  wwlksubclwwlk  27208  smcnlem  27879  nmoub3i  27955  ubthlem3  28055  minvecolem2  28058  minvecolem3  28059  minvecolem4  28063  htthlem  28101  bcs2  28366  pjhthlem1  28577  cnlnadjlem2  29254  cnlnadjlem7  29259  nmopadjlem  29275  nmoptrii  29280  nmopcoadji  29287  leopnmid  29324  cdj1i  29619  nndiffz1  29874  pmtrto1cl  30173  psgnfzto1stlem  30174  fzto1st  30177  psgnfzto1st  30179  smatrcl  30186  submateqlem1  30197  nexple  30395  esumpcvgval  30464  oddpwdc  30740  eulerpartlems  30746  eulerpartlemgc  30748  eulerpartlemb  30754  dstfrvunirn  30860  orvclteinc  30861  ballotlemsima  30901  ballotlemfrcn0  30915  signstfveq0  30978  fsum2dsub  31009  breprexplemc  31034  breprexp  31035  logdivsqrle  31052  hgt750lemb  31058  hgt750leme  31060  tgoldbachgnn  31061  dnibndlem2  32784  dnibndlem6  32788  dnibndlem9  32791  dnibndlem10  32792  dnibndlem11  32793  dnibndlem12  32794  knoppcnlem4  32801  unblimceq0lem  32812  unblimceq0  32813  unbdqndv2lem2  32816  knoppndvlem11  32828  knoppndvlem14  32831  knoppndvlem15  32832  knoppndvlem18  32835  knoppndvlem21  32838  poimirlem6  33726  poimirlem7  33727  poimirlem13  33733  poimirlem15  33735  poimirlem29  33749  mblfinlem2  33758  mblfinlem3  33759  mblfinlem4  33760  ismblfin  33761  itg2addnc  33774  iblmulc2nc  33785  bddiblnc  33790  ftc1anclem7  33801  ftc1anclem8  33802  filbcmb  33845  geomcau  33864  prdsbnd  33901  cntotbnd  33904  bfplem2  33931  rrntotbnd  33944  iccbnd  33948  lzunuz  37830  irrapxlem3  37887  irrapxlem4  37888  irrapxlem5  37889  pellexlem2  37893  pell1qrge1  37933  monotoddzzfi  38005  jm2.17a  38025  rmygeid  38029  fzmaxdif  38046  jm2.27c  38072  jm3.1lem1  38082  expdiophlem1  38086  imo72b2lem0  38962  int-ineqtransd  38994  dvgrat  39008  monoords  39989  absnpncan2d  39994  absnpncan3d  39999  ssfiunibd  40001  leadd12dd  40009  rexabslelem  40121  uzublem  40133  sqrlearg  40257  fmul01  40289  fmul01lt1lem1  40293  fmul01lt1lem2  40294  climsuselem1  40316  climsuse  40317  limsupresico  40409  limsupubuzlem  40421  limsupmnfuzlem  40435  limsupre3uzlem  40444  liminfresico  40480  limsup10exlem  40481  cnrefiisplem  40532  dvdivbd  40615  dvbdfbdioolem2  40621  ioodvbdlimc1lem1  40623  ioodvbdlimc1lem2  40624  ioodvbdlimc2lem  40626  dvnmul  40635  dvnprodlem1  40638  dvnprodlem2  40639  iblspltprt  40665  itgspltprt  40671  stoweidlem1  40694  stoweidlem3  40696  stoweidlem5  40698  stoweidlem11  40704  stoweidlem17  40710  stoweidlem20  40713  stoweidlem26  40719  stoweidlem34  40727  wallispilem4  40761  stirlinglem11  40777  stirlinglem12  40778  stirlinglem13  40779  fourierdlem12  40812  fourierdlem15  40815  fourierdlem20  40820  fourierdlem30  40830  fourierdlem39  40839  fourierdlem42  40842  fourierdlem47  40846  fourierdlem50  40849  fourierdlem64  40863  fourierdlem65  40864  fourierdlem68  40867  fourierdlem73  40872  fourierdlem77  40876  fourierdlem79  40878  fourierdlem87  40886  elaa2lem  40926  etransclem23  40950  ioorrnopnlem  41000  salgencntex  41037  sge0le  41100  sge0isum  41120  sge0xaddlem1  41126  hoicvr  41241  hsphoidmvle2  41278  hoidmv1lelem1  41284  hoidmv1lelem2  41285  hoidmv1lelem3  41286  hoidmvlelem1  41288  hoidmvlelem2  41289  hoidmvlelem4  41291  hspmbllem1  41319  hspmbllem2  41320  smfmullem1  41477  smfmullem2  41478  smfmullem3  41479  smfsuplem1  41496  lighneallem4a  42097  fllog2  42927