Theorem letrd 11307

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043   ≤ cle 11185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-pre-lttri 11118  ax-pre-lttrn 11119

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190

This theorem is referenced by:  lesub3d  11772  le2addd  11773  supmul1  12128  supmul  12131  nn0negleid  12470  eluzuzle  12778  iccsplit  13422  supicc  13438  fzdisj  13488  ssfzunsnext  13506  difelfzle  13578  flwordi  13750  flleceil  13791  uzsup  13801  modltm1p1mod  13864  seqf1olem1  13982  zzlesq  14147  bernneq  14170  bernneq3  14172  discr1  14180  faclbnd  14231  faclbnd4lem1  14234  facubnd  14241  seqcoll  14405  01sqrexlem7  15190  absle  15258  releabs  15264  absrdbnd  15284  rexuzre  15295  limsupgre  15423  lo1bddrp  15467  rlimclim1  15487  rlimresb  15507  rlimrege0  15521  o1add  15556  o1sub  15558  climsqz  15583  climsqz2  15584  rlimsqzlem  15591  rlimsqz  15592  rlimsqz2  15593  rlimno1  15596  isercoll  15610  caucvgrlem  15615  iseraltlem3  15626  o1fsum  15755  cvgcmp  15758  cvgcmpce  15760  climcnds  15793  expcnv  15806  cvgrat  15825  mertenslem2  15827  fprodle  15938  eftlub  16053  rpnnen2lem12  16169  bitsfzo  16381  isprm5  16653  isprm7  16654  eulerthlem2  16728  pcmpt2  16840  pcfac  16846  prmreclem3  16865  prmreclem4  16866  prmreclem5  16867  4sqlem11  16902  vdwlem1  16928  vdwlem3  16930  setsstruct2  17120  prdsxmetlem  24289  nrmmetd  24495  nm2dif  24546  nlmvscnlem2  24606  nmoco  24658  nmotri  24660  nghmcn  24666  icccmplem2  24745  reconnlem2  24749  elii1  24864  xrhmeo  24877  cnheiborlem  24886  bndth  24890  tcphcphlem1  25168  ipcnlem2  25177  cncmet  25255  trirn  25333  minveclem2  25359  minveclem4  25365  ivthlem2  25386  ovolunlem1a  25430  ovolunlem1  25431  ovolfiniun  25435  ovoliunlem1  25436  ovolicc2lem4  25454  ovolicc2lem5  25455  ovolicopnf  25458  nulmbl2  25470  ioombl1lem4  25495  ioorcl2  25506  uniioombllem3  25519  uniioombllem4  25520  uniioombllem5  25521  volcn  25540  vitalilem2  25543  vitali  25547  mbfi1fseqlem5  25653  mbfi1fseqlem6  25654  itg2splitlem  25682  itg2monolem1  25684  itg2monolem3  25686  itg2mono  25687  itg2cnlem1  25695  itgle  25744  bddmulibl  25773  bddiblnc  25776  ditgsplitlem  25794  dveflem  25916  dvlip  25931  dveq0  25938  dvfsumabs  25962  dvfsumlem1  25965  dvfsumlem2  25966  dvfsumlem2OLD  25967  dvfsumlem3  25968  dvfsumlem4  25969  dvfsum2  25974  fta1glem2  26107  dgradd2  26207  plydiveu  26239  fta1lem  26248  aalioulem2  26274  aalioulem3  26275  aalioulem4  26276  aalioulem5  26277  aaliou3lem8  26286  aaliou3lem9  26291  ulmbdd  26340  ulmcn  26341  mtest  26346  mtestbdd  26347  abelthlem2  26375  abelthlem7  26381  pilem2  26395  tanabsge  26448  cosordlem  26472  tanord  26480  logneg2  26557  abslogle  26560  dvlog2lem  26594  cxple2a  26641  abscxpbnd  26696  atans2  26874  leibpi  26885  o1cxp  26918  cxploglim2  26922  jensenlem2  26931  emcllem6  26944  harmoniclbnd  26952  harmonicubnd  26953  harmonicbnd4  26954  fsumharmonic  26955  lgamgulmlem2  26973  lgamgulmlem3  26974  lgamgulmlem5  26976  lgambdd  26980  ftalem2  27017  basellem3  27026  basellem5  27028  basellem6  27029  dvdsflsumcom  27131  fsumfldivdiaglem  27132  ppiub  27148  chtublem  27155  logfac2  27161  chpub  27164  logfacubnd  27165  logfaclbnd  27166  logfacbnd3  27167  logexprlim  27169  bcmono  27221  bpos1lem  27226  bposlem1  27228  bposlem2  27229  bposlem3  27230  bposlem4  27231  bposlem5  27232  bposlem6  27233  bposlem7  27234  bposlem9  27236  lgsdirprm  27275  lgsquadlem1  27324  2lgslem1c  27337  2sqlem8  27370  chebbnd1lem1  27413  chebbnd1lem3  27415  chtppilimlem1  27417  chpchtlim  27423  vmadivsumb  27427  rplogsumlem1  27428  rplogsumlem2  27429  rpvmasumlem  27431  dchrisumlema  27432  dchrisumlem2  27434  dchrisumlem3  27435  dchrmusum2  27438  dchrvmasumlem2  27442  dchrvmasumlem3  27443  dchrvmasumlema  27444  dchrvmasumiflem1  27445  dchrisum0flblem1  27452  dchrisum0flblem2  27453  dchrisum0fno1  27455  dchrisum0re  27457  dchrisum0lem1b  27459  dchrisum0lem1  27460  dchrisum0lem2a  27461  dchrisum0  27464  rplogsum  27471  mudivsum  27474  mulogsumlem  27475  logdivsum  27477  mulog2sumlem1  27478  mulog2sumlem2  27479  2vmadivsumlem  27484  log2sumbnd  27488  selberglem2  27490  selbergb  27493  selberg2lem  27494  selberg2b  27496  chpdifbndlem1  27497  logdivbnd  27500  selberg3lem1  27501  selberg3lem2  27502  selberg4lem1  27504  pntrmax  27508  pntrsumo1  27509  pntrsumbnd  27510  pntrlog2bndlem1  27521  pntrlog2bndlem2  27522  pntrlog2bndlem3  27523  pntrlog2bndlem5  27525  pntrlog2bndlem6  27527  pntrlog2bnd  27528  pntpbnd1a  27529  pntpbnd1  27530  pntpbnd2  27531  pntibndlem2  27535  pntibndlem3  27536  pntlemg  27542  pntlemr  27546  pntlemj  27547  pntlemf  27549  pntlemk  27550  pntlemo  27551  pntleml  27555  abvcxp  27559  qabvle  27569  padicabv  27574  ostth2lem2  27578  ostth2lem3  27579  ostth3  27582  axlowdimlem16  28937  axcontlem8  28951  axcontlem10  28953  wwlksm1edg  29861  wwlksubclwwlk  30037  smcnlem  30676  nmoub3i  30752  ubthlem3  30851  minvecolem2  30854  minvecolem3  30855  minvecolem4  30859  htthlem  30896  bcs2  31161  pjhthlem1  31370  cnlnadjlem2  32047  cnlnadjlem7  32052  nmopadjlem  32068  nmoptrii  32073  nmopcoadji  32080  leopnmid  32117  cdj1i  32412  nndiffz1  32759  nexple  32819  oexpled  32822  pmtrto1cl  33071  psgnfzto1stlem  33072  fzto1st  33075  psgnfzto1st  33077  cyc3conja  33129  constrresqrtcl  33760  cos9thpiminplylem1  33765  smatrcl  33779  submateqlem1  33790  esumpcvgval  34061  oddpwdc  34338  eulerpartlems  34344  eulerpartlemgc  34346  eulerpartlemb  34352  dstfrvunirn  34459  orvclteinc  34460  ballotlemsima  34500  ballotlemfrcn0  34514  signstfveq0  34561  fsum2dsub  34591  breprexplemc  34616  breprexp  34617  logdivsqrle  34634  hgt750lemb  34640  hgt750leme  34642  tgoldbachgnn  34643  dnibndlem2  36460  dnibndlem6  36464  dnibndlem9  36467  dnibndlem10  36468  dnibndlem11  36469  dnibndlem12  36470  knoppcnlem4  36477  unblimceq0lem  36487  unblimceq0  36488  unbdqndv2lem2  36491  knoppndvlem11  36503  knoppndvlem14  36506  knoppndvlem15  36507  knoppndvlem18  36510  knoppndvlem21  36513  poimirlem6  37613  poimirlem7  37614  poimirlem13  37620  poimirlem15  37622  poimirlem29  37636  mblfinlem2  37645  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  itg2addnc  37661  iblmulc2nc  37672  ftc1anclem7  37686  ftc1anclem8  37687  filbcmb  37727  geomcau  37746  prdsbnd  37780  cntotbnd  37783  bfplem2  37810  rrntotbnd  37823  iccbnd  37827  lcmineqlem20  42029  lcmineqlem21  42030  lcmineqlem22  42031  3lexlogpow5ineq2  42036  3lexlogpow5ineq5  42041  aks4d1p1p2  42051  aks4d1p1p4  42052  aks4d1p1p7  42055  aks4d1p1p5  42056  aks4d1p1  42057  aks4d1p2  42058  aks4d1p3  42059  aks4d1p5  42061  aks4d1p6  42062  aks4d1p7d1  42063  aks4d1p7  42064  aks4d1p8  42068  posbezout  42081  aks6d1c1  42097  aks6d1c2lem4  42108  2np3bcnp1  42125  sticksstones6  42132  sticksstones7  42133  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  bcled  42159  bcle2d  42160  aks6d1c7lem1  42161  aks6d1c7lem2  42162  unitscyglem4  42179  lzunuz  42749  irrapxlem3  42805  irrapxlem4  42806  irrapxlem5  42807  pellexlem2  42811  pell1qrge1  42851  monotoddzzfi  42924  jm2.17a  42942  rmygeid  42946  fzmaxdif  42963  jm2.27c  42989  jm3.1lem1  42999  expdiophlem1  43003  fzunt  43437  fzuntd  43438  fzunt1d  43439  fzuntgd  43440  imo72b2lem0  44147  int-ineqtransd  44176  dvgrat  44294  monoords  45288  absnpncan2d  45293  absnpncan3d  45298  ssfiunibd  45300  rexabslelem  45407  uzublem  45419  sqrlearg  45544  fmul01  45571  fmul01lt1lem1  45575  fmul01lt1lem2  45576  climsuselem1  45598  climsuse  45599  limsupresico  45691  limsupubuzlem  45703  limsupmnfuzlem  45717  limsupre3uzlem  45726  liminfresico  45762  limsup10exlem  45763  cnrefiisplem  45820  dvdivbd  45914  dvbdfbdioolem2  45920  ioodvbdlimc1lem1  45922  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnmul  45934  dvnprodlem1  45937  dvnprodlem2  45938  iblspltprt  45964  itgspltprt  45970  stoweidlem1  45992  stoweidlem3  45994  stoweidlem5  45996  stoweidlem11  46002  stoweidlem17  46008  stoweidlem20  46011  stoweidlem26  46017  stoweidlem34  46025  wallispilem4  46059  stirlinglem11  46075  stirlinglem12  46076  stirlinglem13  46077  fourierdlem12  46110  fourierdlem15  46113  fourierdlem20  46118  fourierdlem30  46128  fourierdlem39  46137  fourierdlem42  46140  fourierdlem47  46144  fourierdlem50  46147  fourierdlem64  46161  fourierdlem65  46162  fourierdlem68  46165  fourierdlem73  46170  fourierdlem77  46174  fourierdlem79  46176  fourierdlem87  46184  elaa2lem  46224  etransclem23  46248  ioorrnopnlem  46295  salgencntex  46334  sge0le  46398  sge0isum  46418  sge0xaddlem1  46424  hoicvr  46539  hsphoidmvle2  46576  hoidmv1lelem1  46582  hoidmv1lelem2  46583  hoidmv1lelem3  46584  hoidmvlelem1  46586  hoidmvlelem2  46587  hoidmvlelem4  46589  hspmbllem1  46617  hspmbllem2  46618  smfmullem1  46782  smfmullem2  46783  smfmullem3  46784  smfsuplem1  46802  ormkglobd  46866  natglobalincr  46868  2ltceilhalf  47322  ceilhalfnn  47330  modmknepk  47356  lighneallem4a  47602  gpgusgralem  48040  gpgedgvtx1  48046  gpg3kgrtriexlem4  48070  gpg3kgrtriexlem6  48072  fllog2  48550  itcovalt2lem2lem1  48655