Theorem letrd 11474

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 11411	. . 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 2144   class class class wbr 5102  ℝcr 11206   ≤ cle 11351

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pow 5327  ax-pr 5391  ax-un 7755  ax-resscn 11264  ax-pre-lttri 11281  ax-pre-lttrn 11282

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  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 3739  df-csb 3848  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  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 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-er 8724  df-en 8981  df-dom 8982  df-sdom 8983  df-pnf 11352  df-mnf 11353  df-xr 11354  df-ltxr 11355  df-le 11356

This theorem is used by:  lesub3d  11941  le2addd  11942  supmul1  12293  supmul  12296  nn0negleid  12665  eluzuzle  12981  iccsplit  13623  supicc  13639  fzdisj  13692  ssfzunsnext  13710  difelfzle  13782  flwordi  13959  flleceil  14000  uzsup  14010  modltm1p1mod  14073  seqf1olem1  14191  zzlesq  14357  bernneq  14380  bernneq3  14382  discr1  14390  faclbnd  14441  faclbnd4lem1  14444  facubnd  14451  seqcoll  14616  01sqrexlem7  15424  absle  15492  releabs  15498  absrdbnd  15518  rexuzre  15529  limsupgre  15657  lo1bddrp  15701  rlimclim1  15721  rlimresb  15741  rlimrege0  15755  o1add  15790  o1sub  15792  climsqz  15817  climsqz2  15818  rlimsqzlem  15825  rlimsqz  15826  rlimsqz2  15827  rlimno1  15830  isercoll  15844  caucvgrlem  15849  iseraltlem3  15860  o1fsum  15989  cvgcmp  15992  cvgcmpce  15994  climcnds  16029  expcnv  16042  cvgrat  16061  mertenslem2  16063  fprodle  16172  eftlub  16286  rpnnen2lem12  16402  bitsfzo  16614  isprm5  16892  isprm7  16893  eulerthlem2  16968  pcmpt2  17080  pcfac  17086  prmreclem3  17105  prmreclem4  17106  prmreclem5  17107  4sqlem11  17142  vdwlem1  17168  vdwlem3  17170  setsstruct2  17361  prdsxmetlem  24696  nrmmetd  24902  nm2dif  24953  nlmvscnlem2  25013  nmoco  25065  nmotri  25067  nghmcn  25073  icccmplem2  25152  reconnlem2  25156  elii1  25265  xrhmeo  25276  cnheiborlem  25284  bndth  25288  tcphcphlem1  25565  ipcnlem2  25574  cncmet  25652  trirn  25730  minveclem2  25756  minveclem4  25762  ivthlem2  25782  ovolunlem1a  25826  ovolunlem1  25827  ovolfiniun  25831  ovoliunlem1  25832  ovolicc2lem4  25850  ovolicc2lem5  25851  ovolicopnf  25854  nulmbl2  25866  ioombl1lem4  25891  ioorcl2  25902  uniioombllem3  25915  uniioombllem4  25916  uniioombllem5  25917  volcn  25936  vitalilem2  25939  vitali  25943  mbfi1fseqlem5  26049  mbfi1fseqlem6  26050  itg2splitlem  26078  itg2monolem1  26080  itg2monolem3  26082  itg2mono  26083  itg2cnlem1  26091  itgle  26139  bddmulibl  26168  bddiblnc  26171  ditgsplitlem  26189  dveflem  26308  dvlip  26322  dveq0  26329  dvfsumabs  26352  dvfsumlem1  26355  dvfsumlem2  26356  dvfsumlem3  26357  dvfsumlem4  26358  dvfsum2  26363  fta1glem2  26496  dgradd2  26596  plydiveu  26628  fta1lem  26637  aalioulem2  26669  aalioulem3  26670  aalioulem4  26671  aalioulem5  26672  aaliou3lem8  26681  aaliou3lem9  26686  ulmbdd  26734  ulmcn  26735  mtest  26740  mtestbdd  26741  abelthlem2  26768  abelthlem7  26774  pilem2  26788  tanabsge  26844  cosordlem  26867  tanord  26875  logneg2  26952  abslogle  26955  dvlog2lem  26989  cxple2a  27036  abscxpbnd  27090  atans2  27268  leibpi  27279  o1cxp  27311  cxploglim2  27315  jensenlem2  27324  emcllem6  27337  harmoniclbnd  27345  harmonicubnd  27346  harmonicbnd4  27347  fsumharmonic  27348  lgamgulmlem2  27366  lgamgulmlem3  27367  lgamgulmlem5  27369  lgambdd  27373  ftalem2  27410  basellem3  27419  basellem5  27421  basellem6  27422  dvdsflsumcom  27524  fsumfldivdiaglem  27525  ppiub  27540  chtublem  27547  logfac2  27553  chpub  27556  logfacubnd  27557  logfaclbnd  27558  logfacbnd3  27559  logexprlim  27561  bcmono  27613  bpos1lem  27618  bposlem1  27620  bposlem2  27621  bposlem3  27622  bposlem4  27623  bposlem5  27624  bposlem6  27625  bposlem7  27626  bposlem9  27628  lgsdirprm  27667  lgsquadlem1  27716  2lgslem1c  27729  2sqlem8  27762  chebbnd1lem1  27805  chebbnd1lem3  27807  chtppilimlem1  27809  chpchtlim  27815  vmadivsumb  27819  rplogsumlem1  27820  rplogsumlem2  27821  rpvmasumlem  27823  dchrisumlema  27824  dchrisumlem2  27826  dchrisumlem3  27827  dchrmusum2  27830  dchrvmasumlem2  27834  dchrvmasumlem3  27835  dchrvmasumlema  27836  dchrvmasumiflem1  27837  dchrisum0flblem1  27844  dchrisum0flblem2  27845  dchrisum0fno1  27847  dchrisum0re  27849  dchrisum0lem1b  27851  dchrisum0lem1  27852  dchrisum0lem2a  27853  dchrisum0  27856  rplogsum  27863  mudivsum  27866  mulogsumlem  27867  logdivsum  27869  mulog2sumlem1  27870  mulog2sumlem2  27871  2vmadivsumlem  27876  log2sumbnd  27880  selberglem2  27882  selbergb  27885  selberg2lem  27886  selberg2b  27888  chpdifbndlem1  27889  logdivbnd  27892  selberg3lem1  27893  selberg3lem2  27894  selberg4lem1  27896  pntrmax  27900  pntrsumo1  27901  pntrsumbnd  27902  pntrlog2bndlem1  27913  pntrlog2bndlem2  27914  pntrlog2bndlem3  27915  pntrlog2bndlem5  27917  pntrlog2bndlem6  27919  pntrlog2bnd  27920  pntpbnd1a  27921  pntpbnd1  27922  pntpbnd2  27923  pntibndlem2  27927  pntibndlem3  27928  pntlemg  27934  pntlemr  27938  pntlemj  27939  pntlemf  27941  pntlemk  27942  pntlemo  27943  pntleml  27947  abvcxp  27951  qabvle  27961  padicabv  27966  ostth2lem2  27970  ostth2lem3  27971  ostth3  27974  axlowdimlem16  29544  axcontlem8  29558  axcontlem10  29560  wwlksm1edg  30479  wwlksubclwwlk  30658  smcnlem  31308  nmoub3i  31384  ubthlem3  31483  minvecolem2  31486  minvecolem3  31487  minvecolem4  31491  htthlem  31528  bcs2  31793  pjhthlem1  32002  cnlnadjlem2  32679  cnlnadjlem7  32684  nmopadjlem  32700  nmoptrii  32705  nmopcoadji  32712  leopnmid  32749  cdj1i  33044  nndiffz1  33428  nexple  33474  oexpled  33477  pmtrto1cl  33710  psgnfzto1stlem  33711  fzto1st  33714  psgnfzto1st  33716  cyc3conja  33768  constrresqrtcl  34459  cos9thpiminplylem1  34464  smatrcl  34478  submateqlem1  34489  esumpcvgval  34760  oddpwdc  35036  eulerpartlems  35042  eulerpartlemgc  35044  eulerpartlemb  35050  dstfrvunirn  35157  orvclteinc  35158  ballotlemsima  35198  ballotlemfrcn0  35212  signstfveq0  35256  fsum2dsub  35286  breprexplemc  35311  breprexp  35312  logdivsqrle  35329  hgt750lemb  35335  hgt750leme  35337  tgoldbachgnn  35338  dnibndlem2  37441  dnibndlem6  37445  dnibndlem9  37448  dnibndlem10  37449  dnibndlem11  37450  dnibndlem12  37451  knoppcnlem4  37458  unblimceq0lem  37468  unblimceq0  37469  unbdqndv2lem2  37472  knoppndvlem11  37484  knoppndvlem14  37487  knoppndvlem15  37488  knoppndvlem18  37491  knoppndvlem21  37494  poimirlem6  38653  poimirlem7  38654  poimirlem13  38660  poimirlem15  38662  poimirlem29  38676  mblfinlem2  38685  mblfinlem3  38686  mblfinlem4  38687  ismblfin  38688  itg2addnc  38701  iblmulc2nc  38712  ftc1anclem7  38726  ftc1anclem8  38727  filbcmb  38783  geomcau  38802  prdsbnd  38836  cntotbnd  38839  bfplem2  38866  rrntotbnd  38879  iccbnd  38883  lcmineqlem20  43207  lcmineqlem21  43208  lcmineqlem22  43209  3lexlogpow5ineq2  43214  3lexlogpow5ineq5  43219  aks4d1p1p2  43229  aks4d1p1p4  43230  aks4d1p1p7  43233  aks4d1p1p5  43234  aks4d1p1  43235  aks4d1p2  43236  aks4d1p3  43237  aks4d1p5  43239  aks4d1p6  43240  aks4d1p7d1  43241  aks4d1p7  43242  aks4d1p8  43246  posbezout  43259  aks6d1c1  43275  aks6d1c2lem4  43286  2np3bcnp1  43303  sticksstones6  43310  sticksstones7  43311  sticksstones10  43314  sticksstones12a  43316  sticksstones12  43317  sticksstones22  43327  bcled  43337  bcle2d  43338  aks6d1c7lem1  43339  aks6d1c7lem2  43340  unitscyglem4  43357  lzunuz  43888  irrapxlem3  43940  irrapxlem4  43941  irrapxlem5  43942  pellexlem2  43946  pell1qrge1  43986  monotoddzzfi  44058  jm2.17a  44076  rmygeid  44080  fzmaxdif  44097  jm2.27c  44123  jm3.1lem1  44133  expdiophlem1  44137  fzunt  44565  fzuntd  44566  fzunt1d  44567  fzuntgd  44568  imo72b2lem0  45274  int-ineqtransd  45303  dvgrat  45405  monoords  46421  absnpncan2d  46426  absnpncan3d  46431  ssfiunibd  46433  rexabslelem  46536  uzublem  46548  sqrlearg  46673  fmul01  46700  fmul01lt1lem1  46704  fmul01lt1lem2  46705  climsuselem1  46727  climsuse  46728  limsupresico  46818  limsupubuzlem  46830  limsupmnfuzlem  46844  limsupre3uzlem  46853  liminfresico  46889  limsup10exlem  46890  cnrefiisplem  46947  dvdivbd  47041  dvbdfbdioolem2  47047  ioodvbdlimc1lem1  47049  ioodvbdlimc1lem2  47050  ioodvbdlimc2lem  47052  dvnmul  47061  dvnprodlem1  47064  dvnprodlem2  47065  iblspltprt  47091  itgspltprt  47097  stoweidlem1  47119  stoweidlem3  47121  stoweidlem5  47123  stoweidlem11  47129  stoweidlem17  47135  stoweidlem20  47138  stoweidlem26  47144  stoweidlem34  47152  wallispilem4  47186  stirlinglem11  47202  stirlinglem12  47203  stirlinglem13  47204  fourierdlem12  47237  fourierdlem15  47240  fourierdlem20  47245  fourierdlem30  47255  fourierdlem39  47264  fourierdlem42  47267  fourierdlem47  47271  fourierdlem50  47274  fourierdlem64  47288  fourierdlem65  47289  fourierdlem68  47292  fourierdlem73  47297  fourierdlem77  47301  fourierdlem79  47303  fourierdlem87  47311  elaa2lem  47351  etransclem23  47375  ioorrnopnlem  47422  salgencntex  47461  sge0le  47525  sge0isum  47545  sge0xaddlem1  47551  hoicvr  47666  hsphoidmvle2  47703  hoidmv1lelem1  47709  hoidmv1lelem2  47710  hoidmv1lelem3  47711  hoidmvlelem1  47713  hoidmvlelem2  47714  hoidmvlelem4  47716  hspmbllem1  47744  hspmbllem2  47745  smfmullem1  47909  smfmullem2  47910  smfmullem3  47911  smfsuplem1  47929  ormkglobd  47995  2ltceilhalf  48510  ceilhalfnn  48518  modmknepk  48546  lighneallem4a  48801  nprmdvdsfacm1lem4  48816  gpgusgralem  49262  gpgedgvtx1  49268  gpg3kgrtriexlem4  49292  gpg3kgrtriexlem6  49294  fllog2  49788  itcovalt2lem2lem1  49893