Theorem letrd 11302

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037   ≤ cle 11179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184

This theorem is referenced by:  lesub3d  11767  le2addd  11768  supmul1  12123  supmul  12126  nn0negleid  12465  eluzuzle  12772  iccsplit  13413  supicc  13429  fzdisj  13479  ssfzunsnext  13497  difelfzle  13569  flwordi  13744  flleceil  13785  uzsup  13795  modltm1p1mod  13858  seqf1olem1  13976  zzlesq  14141  bernneq  14164  bernneq3  14166  discr1  14174  faclbnd  14225  faclbnd4lem1  14228  facubnd  14235  seqcoll  14399  01sqrexlem7  15183  absle  15251  releabs  15257  absrdbnd  15277  rexuzre  15288  limsupgre  15416  lo1bddrp  15460  rlimclim1  15480  rlimresb  15500  rlimrege0  15514  o1add  15549  o1sub  15551  climsqz  15576  climsqz2  15577  rlimsqzlem  15584  rlimsqz  15585  rlimsqz2  15586  rlimno1  15589  isercoll  15603  caucvgrlem  15608  iseraltlem3  15619  o1fsum  15748  cvgcmp  15751  cvgcmpce  15753  climcnds  15786  expcnv  15799  cvgrat  15818  mertenslem2  15820  fprodle  15931  eftlub  16046  rpnnen2lem12  16162  bitsfzo  16374  isprm5  16646  isprm7  16647  eulerthlem2  16721  pcmpt2  16833  pcfac  16839  prmreclem3  16858  prmreclem4  16859  prmreclem5  16860  4sqlem11  16895  vdwlem1  16921  vdwlem3  16923  setsstruct2  17113  prdsxmetlem  24324  nrmmetd  24530  nm2dif  24581  nlmvscnlem2  24641  nmoco  24693  nmotri  24695  nghmcn  24701  icccmplem2  24780  reconnlem2  24784  elii1  24899  xrhmeo  24912  cnheiborlem  24921  bndth  24925  tcphcphlem1  25203  ipcnlem2  25212  cncmet  25290  trirn  25368  minveclem2  25394  minveclem4  25400  ivthlem2  25421  ovolunlem1a  25465  ovolunlem1  25466  ovolfiniun  25470  ovoliunlem1  25471  ovolicc2lem4  25489  ovolicc2lem5  25490  ovolicopnf  25493  nulmbl2  25505  ioombl1lem4  25530  ioorcl2  25541  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  volcn  25575  vitalilem2  25578  vitali  25582  mbfi1fseqlem5  25688  mbfi1fseqlem6  25689  itg2splitlem  25717  itg2monolem1  25719  itg2monolem3  25721  itg2mono  25722  itg2cnlem1  25730  itgle  25779  bddmulibl  25808  bddiblnc  25811  ditgsplitlem  25829  dveflem  25951  dvlip  25966  dveq0  25973  dvfsumabs  25997  dvfsumlem1  26000  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumlem3  26003  dvfsumlem4  26004  dvfsum2  26009  fta1glem2  26142  dgradd2  26242  plydiveu  26274  fta1lem  26283  aalioulem2  26309  aalioulem3  26310  aalioulem4  26311  aalioulem5  26312  aaliou3lem8  26321  aaliou3lem9  26326  ulmbdd  26375  ulmcn  26376  mtest  26381  mtestbdd  26382  abelthlem2  26410  abelthlem7  26416  pilem2  26430  tanabsge  26483  cosordlem  26507  tanord  26515  logneg2  26592  abslogle  26595  dvlog2lem  26629  cxple2a  26676  abscxpbnd  26731  atans2  26909  leibpi  26920  o1cxp  26953  cxploglim2  26957  jensenlem2  26966  emcllem6  26979  harmoniclbnd  26987  harmonicubnd  26988  harmonicbnd4  26989  fsumharmonic  26990  lgamgulmlem2  27008  lgamgulmlem3  27009  lgamgulmlem5  27011  lgambdd  27015  ftalem2  27052  basellem3  27061  basellem5  27063  basellem6  27064  dvdsflsumcom  27166  fsumfldivdiaglem  27167  ppiub  27183  chtublem  27190  logfac2  27196  chpub  27199  logfacubnd  27200  logfaclbnd  27201  logfacbnd3  27202  logexprlim  27204  bcmono  27256  bpos1lem  27261  bposlem1  27263  bposlem2  27264  bposlem3  27265  bposlem4  27266  bposlem5  27267  bposlem6  27268  bposlem7  27269  bposlem9  27271  lgsdirprm  27310  lgsquadlem1  27359  2lgslem1c  27372  2sqlem8  27405  chebbnd1lem1  27448  chebbnd1lem3  27450  chtppilimlem1  27452  chpchtlim  27458  vmadivsumb  27462  rplogsumlem1  27463  rplogsumlem2  27464  rpvmasumlem  27466  dchrisumlema  27467  dchrisumlem2  27469  dchrisumlem3  27470  dchrmusum2  27473  dchrvmasumlem2  27477  dchrvmasumlem3  27478  dchrvmasumlema  27479  dchrvmasumiflem1  27480  dchrisum0flblem1  27487  dchrisum0flblem2  27488  dchrisum0fno1  27490  dchrisum0re  27492  dchrisum0lem1b  27494  dchrisum0lem1  27495  dchrisum0lem2a  27496  dchrisum0  27499  rplogsum  27506  mudivsum  27509  mulogsumlem  27510  logdivsum  27512  mulog2sumlem1  27513  mulog2sumlem2  27514  2vmadivsumlem  27519  log2sumbnd  27523  selberglem2  27525  selbergb  27528  selberg2lem  27529  selberg2b  27531  chpdifbndlem1  27532  logdivbnd  27535  selberg3lem1  27536  selberg3lem2  27537  selberg4lem1  27539  pntrmax  27543  pntrsumo1  27544  pntrsumbnd  27545  pntrlog2bndlem1  27556  pntrlog2bndlem2  27557  pntrlog2bndlem3  27558  pntrlog2bndlem5  27560  pntrlog2bndlem6  27562  pntrlog2bnd  27563  pntpbnd1a  27564  pntpbnd1  27565  pntpbnd2  27566  pntibndlem2  27570  pntibndlem3  27571  pntlemg  27577  pntlemr  27581  pntlemj  27582  pntlemf  27584  pntlemk  27585  pntlemo  27586  pntleml  27590  abvcxp  27594  qabvle  27604  padicabv  27609  ostth2lem2  27613  ostth2lem3  27614  ostth3  27617  axlowdimlem16  29042  axcontlem8  29056  axcontlem10  29058  wwlksm1edg  29966  wwlksubclwwlk  30145  smcnlem  30785  nmoub3i  30861  ubthlem3  30960  minvecolem2  30963  minvecolem3  30964  minvecolem4  30968  htthlem  31005  bcs2  31270  pjhthlem1  31479  cnlnadjlem2  32156  cnlnadjlem7  32161  nmopadjlem  32177  nmoptrii  32182  nmopcoadji  32189  leopnmid  32226  cdj1i  32521  nndiffz1  32877  nexple  32936  oexpled  32939  pmtrto1cl  33193  psgnfzto1stlem  33194  fzto1st  33197  psgnfzto1st  33199  cyc3conja  33251  constrresqrtcl  33955  cos9thpiminplylem1  33960  smatrcl  33974  submateqlem1  33985  esumpcvgval  34256  oddpwdc  34532  eulerpartlems  34538  eulerpartlemgc  34540  eulerpartlemb  34546  dstfrvunirn  34653  orvclteinc  34654  ballotlemsima  34694  ballotlemfrcn0  34708  signstfveq0  34755  fsum2dsub  34785  breprexplemc  34810  breprexp  34811  logdivsqrle  34828  hgt750lemb  34834  hgt750leme  34836  tgoldbachgnn  34837  dnibndlem2  36701  dnibndlem6  36705  dnibndlem9  36708  dnibndlem10  36709  dnibndlem11  36710  dnibndlem12  36711  knoppcnlem4  36718  unblimceq0lem  36728  unblimceq0  36729  unbdqndv2lem2  36732  knoppndvlem11  36744  knoppndvlem14  36747  knoppndvlem15  36748  knoppndvlem18  36751  knoppndvlem21  36754  poimirlem6  37877  poimirlem7  37878  poimirlem13  37884  poimirlem15  37886  poimirlem29  37900  mblfinlem2  37909  mblfinlem3  37910  mblfinlem4  37911  ismblfin  37912  itg2addnc  37925  iblmulc2nc  37936  ftc1anclem7  37950  ftc1anclem8  37951  filbcmb  37991  geomcau  38010  prdsbnd  38044  cntotbnd  38047  bfplem2  38074  rrntotbnd  38087  iccbnd  38091  lcmineqlem20  42418  lcmineqlem21  42419  lcmineqlem22  42420  3lexlogpow5ineq2  42425  3lexlogpow5ineq5  42430  aks4d1p1p2  42440  aks4d1p1p4  42441  aks4d1p1p7  42444  aks4d1p1p5  42445  aks4d1p1  42446  aks4d1p2  42447  aks4d1p3  42448  aks4d1p5  42450  aks4d1p6  42451  aks4d1p7d1  42452  aks4d1p7  42453  aks4d1p8  42457  posbezout  42470  aks6d1c1  42486  aks6d1c2lem4  42497  2np3bcnp1  42514  sticksstones6  42521  sticksstones7  42522  sticksstones10  42525  sticksstones12a  42527  sticksstones12  42528  sticksstones22  42538  bcled  42548  bcle2d  42549  aks6d1c7lem1  42550  aks6d1c7lem2  42551  unitscyglem4  42568  lzunuz  43125  irrapxlem3  43181  irrapxlem4  43182  irrapxlem5  43183  pellexlem2  43187  pell1qrge1  43227  monotoddzzfi  43299  jm2.17a  43317  rmygeid  43321  fzmaxdif  43338  jm2.27c  43364  jm3.1lem1  43374  expdiophlem1  43378  fzunt  43811  fzuntd  43812  fzunt1d  43813  fzuntgd  43814  imo72b2lem0  44521  int-ineqtransd  44550  dvgrat  44668  monoords  45659  absnpncan2d  45664  absnpncan3d  45669  ssfiunibd  45671  rexabslelem  45776  uzublem  45788  sqrlearg  45913  fmul01  45940  fmul01lt1lem1  45944  fmul01lt1lem2  45945  climsuselem1  45967  climsuse  45968  limsupresico  46058  limsupubuzlem  46070  limsupmnfuzlem  46084  limsupre3uzlem  46093  liminfresico  46129  limsup10exlem  46130  cnrefiisplem  46187  dvdivbd  46281  dvbdfbdioolem2  46287  ioodvbdlimc1lem1  46289  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  dvnmul  46301  dvnprodlem1  46304  dvnprodlem2  46305  iblspltprt  46331  itgspltprt  46337  stoweidlem1  46359  stoweidlem3  46361  stoweidlem5  46363  stoweidlem11  46369  stoweidlem17  46375  stoweidlem20  46378  stoweidlem26  46384  stoweidlem34  46392  wallispilem4  46426  stirlinglem11  46442  stirlinglem12  46443  stirlinglem13  46444  fourierdlem12  46477  fourierdlem15  46480  fourierdlem20  46485  fourierdlem30  46495  fourierdlem39  46504  fourierdlem42  46507  fourierdlem47  46511  fourierdlem50  46514  fourierdlem64  46528  fourierdlem65  46529  fourierdlem68  46532  fourierdlem73  46537  fourierdlem77  46541  fourierdlem79  46543  fourierdlem87  46551  elaa2lem  46591  etransclem23  46615  ioorrnopnlem  46662  salgencntex  46701  sge0le  46765  sge0isum  46785  sge0xaddlem1  46791  hoicvr  46906  hsphoidmvle2  46943  hoidmv1lelem1  46949  hoidmv1lelem2  46950  hoidmv1lelem3  46951  hoidmvlelem1  46953  hoidmvlelem2  46954  hoidmvlelem4  46956  hspmbllem1  46984  hspmbllem2  46985  smfmullem1  47149  smfmullem2  47150  smfmullem3  47151  smfsuplem1  47169  ormkglobd  47233  natglobalincr  47235  2ltceilhalf  47688  ceilhalfnn  47696  modmknepk  47722  lighneallem4a  47968  gpgusgralem  48416  gpgedgvtx1  48422  gpg3kgrtriexlem4  48446  gpg3kgrtriexlem6  48448  fllog2  48928  itcovalt2lem2lem1  49033