Theorem letrd 11366

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149   class class class wbr 5113  ℝcr 11098   ≤ cle 11243

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-resscn 11156  ax-pre-lttri 11173  ax-pre-lttrn 11174

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  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 8693  df-en 8943  df-dom 8944  df-sdom 8945  df-pnf 11244  df-mnf 11245  df-xr 11246  df-ltxr 11247  df-le 11248

This theorem is referenced by:  lesub3d  11831  le2addd  11832  supmul1  12183  supmul  12186  nn0negleid  12555  eluzuzle  12870  iccsplit  13511  supicc  13527  fzdisj  13578  ssfzunsnext  13596  difelfzle  13668  flwordi  13844  flleceil  13885  uzsup  13895  modltm1p1mod  13958  seqf1olem1  14076  zzlesq  14241  bernneq  14264  bernneq3  14266  discr1  14274  faclbnd  14325  faclbnd4lem1  14328  facubnd  14335  seqcoll  14500  01sqrexlem7  15298  absle  15366  releabs  15372  absrdbnd  15392  rexuzre  15403  limsupgre  15531  lo1bddrp  15575  rlimclim1  15595  rlimresb  15615  rlimrege0  15629  o1add  15664  o1sub  15666  climsqz  15691  climsqz2  15692  rlimsqzlem  15699  rlimsqz  15700  rlimsqz2  15701  rlimno1  15704  isercoll  15718  caucvgrlem  15723  iseraltlem3  15734  o1fsum  15864  cvgcmp  15867  cvgcmpce  15869  climcnds  15904  expcnv  15917  cvgrat  15936  mertenslem2  15938  fprodle  16049  eftlub  16164  rpnnen2lem12  16280  bitsfzo  16492  isprm5  16765  isprm7  16766  eulerthlem2  16840  pcmpt2  16952  pcfac  16958  prmreclem3  16977  prmreclem4  16978  prmreclem5  16979  4sqlem11  17014  vdwlem1  17040  vdwlem3  17042  setsstruct2  17233  prdsxmetlem  24493  nrmmetd  24699  nm2dif  24750  nlmvscnlem2  24810  nmoco  24862  nmotri  24864  nghmcn  24870  icccmplem2  24949  reconnlem2  24953  elii1  25062  xrhmeo  25073  cnheiborlem  25081  bndth  25085  tcphcphlem1  25362  ipcnlem2  25371  cncmet  25449  trirn  25527  minveclem2  25553  minveclem4  25559  ivthlem2  25579  ovolunlem1a  25623  ovolunlem1  25624  ovolfiniun  25628  ovoliunlem1  25629  ovolicc2lem4  25647  ovolicc2lem5  25648  ovolicopnf  25651  nulmbl2  25663  ioombl1lem4  25688  ioorcl2  25699  uniioombllem3  25712  uniioombllem4  25713  uniioombllem5  25714  volcn  25733  vitalilem2  25736  vitali  25740  mbfi1fseqlem5  25846  mbfi1fseqlem6  25847  itg2splitlem  25875  itg2monolem1  25877  itg2monolem3  25879  itg2mono  25880  itg2cnlem1  25888  itgle  25937  bddmulibl  25966  bddiblnc  25969  ditgsplitlem  25987  dveflem  26106  dvlip  26120  dveq0  26127  dvfsumabs  26150  dvfsumlem1  26153  dvfsumlem2  26154  dvfsumlem3  26155  dvfsumlem4  26156  dvfsum2  26161  fta1glem2  26294  dgradd2  26393  plydiveu  26427  fta1lem  26436  aalioulem2  26462  aalioulem3  26463  aalioulem4  26464  aalioulem5  26465  aaliou3lem8  26474  aaliou3lem9  26479  ulmbdd  26526  ulmcn  26527  mtest  26532  mtestbdd  26533  abelthlem2  26560  abelthlem7  26566  pilem2  26580  tanabsge  26636  cosordlem  26660  tanord  26668  logneg2  26745  abslogle  26748  dvlog2lem  26782  cxple2a  26829  abscxpbnd  26883  atans2  27061  leibpi  27072  o1cxp  27104  cxploglim2  27108  jensenlem2  27117  emcllem6  27130  harmoniclbnd  27138  harmonicubnd  27139  harmonicbnd4  27140  fsumharmonic  27141  lgamgulmlem2  27159  lgamgulmlem3  27160  lgamgulmlem5  27162  lgambdd  27166  ftalem2  27203  basellem3  27212  basellem5  27214  basellem6  27215  dvdsflsumcom  27317  fsumfldivdiaglem  27318  ppiub  27333  chtublem  27340  logfac2  27346  chpub  27349  logfacubnd  27350  logfaclbnd  27351  logfacbnd3  27352  logexprlim  27354  bcmono  27406  bpos1lem  27411  bposlem1  27413  bposlem2  27414  bposlem3  27415  bposlem4  27416  bposlem5  27417  bposlem6  27418  bposlem7  27419  bposlem9  27421  lgsdirprm  27460  lgsquadlem1  27509  2lgslem1c  27522  2sqlem8  27555  chebbnd1lem1  27598  chebbnd1lem3  27600  chtppilimlem1  27602  chpchtlim  27608  vmadivsumb  27612  rplogsumlem1  27613  rplogsumlem2  27614  rpvmasumlem  27616  dchrisumlema  27617  dchrisumlem2  27619  dchrisumlem3  27620  dchrmusum2  27623  dchrvmasumlem2  27627  dchrvmasumlem3  27628  dchrvmasumlema  27629  dchrvmasumiflem1  27630  dchrisum0flblem1  27637  dchrisum0flblem2  27638  dchrisum0fno1  27640  dchrisum0re  27642  dchrisum0lem1b  27644  dchrisum0lem1  27645  dchrisum0lem2a  27646  dchrisum0  27649  rplogsum  27656  mudivsum  27659  mulogsumlem  27660  logdivsum  27662  mulog2sumlem1  27663  mulog2sumlem2  27664  2vmadivsumlem  27669  log2sumbnd  27673  selberglem2  27675  selbergb  27678  selberg2lem  27679  selberg2b  27681  chpdifbndlem1  27682  logdivbnd  27685  selberg3lem1  27686  selberg3lem2  27687  selberg4lem1  27689  pntrmax  27693  pntrsumo1  27694  pntrsumbnd  27695  pntrlog2bndlem1  27706  pntrlog2bndlem2  27707  pntrlog2bndlem3  27708  pntrlog2bndlem5  27710  pntrlog2bndlem6  27712  pntrlog2bnd  27713  pntpbnd1a  27714  pntpbnd1  27715  pntpbnd2  27716  pntibndlem2  27720  pntibndlem3  27721  pntlemg  27727  pntlemr  27731  pntlemj  27732  pntlemf  27734  pntlemk  27735  pntlemo  27736  pntleml  27740  abvcxp  27744  qabvle  27754  padicabv  27759  ostth2lem2  27763  ostth2lem3  27764  ostth3  27767  axlowdimlem16  29247  axcontlem8  29261  axcontlem10  29263  wwlksm1edg  30170  wwlksubclwwlk  30349  smcnlem  30989  nmoub3i  31065  ubthlem3  31164  minvecolem2  31167  minvecolem3  31168  minvecolem4  31172  htthlem  31209  bcs2  31474  pjhthlem1  31683  cnlnadjlem2  32360  cnlnadjlem7  32365  nmopadjlem  32381  nmoptrii  32386  nmopcoadji  32393  leopnmid  32430  cdj1i  32725  nndiffz1  33071  nexple  33117  oexpled  33120  pmtrto1cl  33359  psgnfzto1stlem  33360  fzto1st  33363  psgnfzto1st  33365  cyc3conja  33417  constrresqrtcl  34111  cos9thpiminplylem1  34116  smatrcl  34130  submateqlem1  34141  esumpcvgval  34412  oddpwdc  34688  eulerpartlems  34694  eulerpartlemgc  34696  eulerpartlemb  34702  dstfrvunirn  34809  orvclteinc  34810  ballotlemsima  34850  ballotlemfrcn0  34864  signstfveq0  34908  fsum2dsub  34938  breprexplemc  34963  breprexp  34964  logdivsqrle  34981  hgt750lemb  34987  hgt750leme  34989  tgoldbachgnn  34990  dnibndlem2  36956  dnibndlem6  36960  dnibndlem9  36963  dnibndlem10  36964  dnibndlem11  36965  dnibndlem12  36966  knoppcnlem4  36973  unblimceq0lem  36983  unblimceq0  36984  unbdqndv2lem2  36987  knoppndvlem11  36999  knoppndvlem14  37002  knoppndvlem15  37003  knoppndvlem18  37006  knoppndvlem21  37009  poimirlem6  38164  poimirlem7  38165  poimirlem13  38171  poimirlem15  38173  poimirlem29  38187  mblfinlem2  38196  mblfinlem3  38197  mblfinlem4  38198  ismblfin  38199  itg2addnc  38212  iblmulc2nc  38223  ftc1anclem7  38237  ftc1anclem8  38238  filbcmb  38278  geomcau  38297  prdsbnd  38331  cntotbnd  38334  bfplem2  38361  rrntotbnd  38374  iccbnd  38378  lcmineqlem20  42704  lcmineqlem21  42705  lcmineqlem22  42706  3lexlogpow5ineq2  42711  3lexlogpow5ineq5  42716  aks4d1p1p2  42726  aks4d1p1p4  42727  aks4d1p1p7  42730  aks4d1p1p5  42731  aks4d1p1  42732  aks4d1p2  42733  aks4d1p3  42734  aks4d1p5  42736  aks4d1p6  42737  aks4d1p7d1  42738  aks4d1p7  42739  aks4d1p8  42743  posbezout  42756  aks6d1c1  42772  aks6d1c2lem4  42783  2np3bcnp1  42800  sticksstones6  42807  sticksstones7  42808  sticksstones10  42811  sticksstones12a  42813  sticksstones12  42814  sticksstones22  42824  bcled  42834  bcle2d  42835  aks6d1c7lem1  42836  aks6d1c7lem2  42837  unitscyglem4  42854  lzunuz  43390  irrapxlem3  43442  irrapxlem4  43443  irrapxlem5  43444  pellexlem2  43448  pell1qrge1  43488  monotoddzzfi  43560  jm2.17a  43578  rmygeid  43582  fzmaxdif  43599  jm2.27c  43625  jm3.1lem1  43635  expdiophlem1  43639  fzunt  44072  fzuntd  44073  fzunt1d  44074  fzuntgd  44075  imo72b2lem0  44782  int-ineqtransd  44811  dvgrat  44913  monoords  45907  absnpncan2d  45912  absnpncan3d  45917  ssfiunibd  45919  rexabslelem  46023  uzublem  46035  sqrlearg  46160  fmul01  46187  fmul01lt1lem1  46191  fmul01lt1lem2  46192  climsuselem1  46214  climsuse  46215  limsupresico  46305  limsupubuzlem  46317  limsupmnfuzlem  46331  limsupre3uzlem  46340  liminfresico  46376  limsup10exlem  46377  cnrefiisplem  46434  dvdivbd  46528  dvbdfbdioolem2  46534  ioodvbdlimc1lem1  46536  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  dvnmul  46548  dvnprodlem1  46551  dvnprodlem2  46552  iblspltprt  46578  itgspltprt  46584  stoweidlem1  46606  stoweidlem3  46608  stoweidlem5  46610  stoweidlem11  46616  stoweidlem17  46622  stoweidlem20  46625  stoweidlem26  46631  stoweidlem34  46639  wallispilem4  46673  stirlinglem11  46689  stirlinglem12  46690  stirlinglem13  46691  fourierdlem12  46724  fourierdlem15  46727  fourierdlem20  46732  fourierdlem30  46742  fourierdlem39  46751  fourierdlem42  46754  fourierdlem47  46758  fourierdlem50  46761  fourierdlem64  46775  fourierdlem65  46776  fourierdlem68  46779  fourierdlem73  46784  fourierdlem77  46788  fourierdlem79  46790  fourierdlem87  46798  elaa2lem  46838  etransclem23  46862  ioorrnopnlem  46909  salgencntex  46948  sge0le  47012  sge0isum  47032  sge0xaddlem1  47038  hoicvr  47153  hsphoidmvle2  47190  hoidmv1lelem1  47196  hoidmv1lelem2  47197  hoidmv1lelem3  47198  hoidmvlelem1  47200  hoidmvlelem2  47201  hoidmvlelem4  47203  hspmbllem1  47231  hspmbllem2  47232  smfmullem1  47396  smfmullem2  47397  smfmullem3  47398  smfsuplem1  47416  ormkglobd  47482  natglobalincr  47484  2ltceilhalf  47957  ceilhalfnn  47965  modmknepk  47993  lighneallem4a  48248  nprmdvdsfacm1lem4  48263  gpgusgralem  48709  gpgedgvtx1  48715  gpg3kgrtriexlem4  48739  gpg3kgrtriexlem6  48741  fllog2  49232  itcovalt2lem2lem1  49337