Theorem ltled 11353

Description: 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
ltled.1	⊢ (𝜑 → 𝐴 < 𝐵)

Assertion

Ref	Expression
ltled	⊢ (𝜑 → 𝐴 ≤ 𝐵)

Proof of Theorem ltled

Step	Hyp	Ref	Expression
1		ltled.1	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
2		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4		ltle 11293	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
5	2, 3, 4	syl2anc 595	. 2 ⊢ (𝜑 → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
6	1, 5	mpd 16	1 ⊢ (𝜑 → 𝐴 ≤ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5109  ℝcr 11094   < clt 11238   ≤ cle 11239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-resscn 11152  ax-pre-lttri 11169

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-pnf 11240  df-mnf 11241  df-xr 11242  df-ltxr 11243  df-le 11244

This theorem is referenced by:  ltnsymd  11354  mulge0  11727  msqge0  11730  addgt0d  11784  lt2addd  11832  lt2msq1  12094  uzwo3  12962  fznatpl1  13602  flflp1  13836  modaddmodup  13966  expmulnbnd  14267  fzsdom2  14461  repswcshw  14845  sgnmul  15140  isercolllem1  15712  caucvgrlem  15720  climcnds  15901  geomulcvg  15926  mertenslem1  15934  ruclem2  16283  ruclem12  16292  bitsfzo  16488  bitsmod  16489  nn0rppwr  16614  nn0expgcd  16617  lcmgcdlem  16659  isprm7  16762  4sqlem7  16999  vdwlem1  17036  chnub  18673  met1stc  24678  cfilucfil  24716  nlmvscnlem2  24842  icccmplem2  24981  reconnlem2  24985  xrhmeo  25105  cnheibor  25114  nmoleub2lem3  25274  ipcnlem2  25403  minveclem3b  25587  ivthlem1  25610  ivthlem2  25611  ivth2  25614  ivthle  25615  ivthle2  25616  ovollb2lem  25647  ovolicc2lem4  25679  ovolicc2lem5  25680  ioombl1lem4  25720  uniioombllem4  25745  uniioombllem5  25746  opnmbllem  25760  ismbf3d  25813  mbfi1fseqlem6  25879  itg2gt0  25919  dveflem  26138  dvferm1lem  26143  dvferm2lem  26145  rollelem  26148  rolle  26149  cmvth  26150  mvth  26151  c1liplem1  26155  dvgt0lem1  26161  dvivthlem1  26167  lhop1lem  26172  lhop1  26173  dvcnvrelem1  26176  dvcnvrelem2  26177  dvcvx  26179  dgradd2  26425  aaliou3lem8  26508  aaliou3lem7  26512  ulmdvlem1  26563  itgulm  26571  radcnvlt1  26581  radcnvle  26583  abelthlem7  26601  efcvx  26612  coseq0negpitopi  26668  tangtx  26670  tanabsge  26671  tanord  26703  abslogimle  26738  divlogrlim  26800  logno1  26801  logcnlem3  26809  logcnlem4  26810  logtayl  26825  logccv  26828  cxple  26860  rtprmirr  26925  chordthmlem4  27000  asinsin  27057  atanlogaddlem  27078  atantan  27088  cxp2limlem  27140  logdifbnd  27158  emcllem4  27163  harmonicbnd4  27175  lgamucov  27202  ftalem1  27237  ftalem2  27238  ftalem3  27239  basellem5  27249  basellem8  27252  chpchtsum  27383  bposlem1  27448  lgseisenlem1  27539  lgsquadlem1  27544  lgsquadlem2  27545  lgsquadlem3  27546  2sqreulem1  27610  2sqreunnlem1  27613  chebbnd1lem2  27634  chebbnd1lem3  27635  chtppilimlem1  27637  chto1ub  27640  chpo1ubb  27645  vmadivsumb  27647  dchrisumlem3  27655  mulog2sumlem1  27698  vmalogdivsum2  27702  vmalogdivsum  27703  2vmadivsumlem  27704  selbergb  27713  selberg2b  27716  chpdifbndlem1  27717  selberg3lem2  27722  selberg3  27723  selberg4lem1  27724  selberg4  27725  pntrsumbnd  27730  selberg3r  27733  selberg4r  27734  selberg34r  27735  pntrlog2bndlem1  27741  pntrlog2bndlem2  27742  pntrlog2bndlem3  27743  pntrlog2bndlem4  27744  pntrlog2bndlem5  27745  pntrlog2bndlem6a  27746  pntrlog2bndlem6  27747  pntrlog2bnd  27748  pntpbnd1a  27749  pntpbnd1  27750  pntpbnd2  27751  pntibndlem2  27755  pntlemb  27761  pntlemq  27765  pntlemr  27766  pntlemj  27767  pntlemf  27769  pntlemp  27774  ostth2lem2  27798  axpaschlem  29290  axlowdimlem16  29307  smcnlem  31049  bcm1n  33140  wrdt2ind  33273  cycpmco2lem6  33451  cyc3conja  33477  smatrcl  34186  fiunelros  34564  dya2icoseg  34667  eulerpartlemgc  34752  dstfrvunirn  34865  ballotlemfc0  34883  ballotlemfcc  34884  ballotlemimin  34896  ballotlemsgt1  34901  ballotlemfrcn0  34920  fdvposlt  34986  breprexp  35020  logdivsqrle  35037  hgt750leme  35045  tgoldbachgt  35050  lpadmax  35072  lpadright  35074  subfacval3  35681  erdszelem8  35690  cvmliftlem6  35782  cvmliftlem7  35783  cvmliftlem8  35784  cvmliftlem9  35785  cvmliftlem10  35786  sinccvglem  36164  dnibndlem9  37075  unbdqndv2lem2  37099  knoppndvlem14  37114  knoppndvlem18  37118  knoppndvlem19  37119  poimirlem7  38278  poimirlem15  38286  opnmbllem0  38307  itg2addnclem  38322  itg2addnclem3  38324  itg2addnc  38325  itg2gt0cn  38326  areacirclem1  38359  areacirc  38364  isbnd3  38435  cntotbnd  38447  rrnequiv  38486  lcmineqlem11  42806  lcmineqlem22  42817  3lexlogpow5ineq2  42822  3lexlogpow5ineq5  42827  dvrelogpow2b  42835  aks4d1p1p2  42837  aks4d1p1p4  42838  aks4d1p1p6  42840  aks4d1p1p7  42841  aks4d1p1p5  42842  aks4d1p1  42843  aks4d1p2  42844  aks4d1p3  42845  aks4d1p5  42847  aks4d1p7d1  42849  aks4d1p7  42850  aks4d1p8  42854  hashscontpow1  42888  aks6d1c2lem4  42894  aks6d1c5lem2  42905  sticksstones6  42918  sticksstones12a  42924  sticksstones12  42925  aks6d1c7lem1  42947  unitscyglem2  42963  posqsqznn  43097  redvmptabs  43121  readvrec  43123  fltnltalem  43394  irrapxlem3  43551  pellexlem2  43557  pellfundglb  43612  monotuz  43668  monotoddzzfi  43669  acongrep  43707  cvgdvgrat  45023  hashnzfz2  45031  hashnzfzclim  45032  binomcxplemnotnn0  45066  monoords  46016  xralrple2  46070  reclt0d  46102  reclt0  46106  uzublem  46144  cvgcaule  46205  iooiinicc  46258  iooiinioc  46272  limciccioolb  46337  limcicciooub  46351  lptre2pt  46354  limsupubuzlem  46426  limsup10exlem  46486  icccncfext  46601  cncfiooicclem1  46607  dvdivbd  46637  dvbdfbdioolem1  46642  dvbdfbdioolem2  46643  ioodvbdlimc1lem2  46646  ioodvbdlimc2lem  46648  dvnxpaek  46656  dvnmul  46657  volioc  46686  iblspltprt  46687  itgspltprt  46693  volico  46697  volioore  46704  voliooico  46706  voliccico  46713  stoweidlem1  46715  stoweidlem3  46717  stoweidlem7  46721  stoweidlem24  46738  stoweidlem26  46740  stoweidlem42  46756  wallispilem5  46783  stirlinglem1  46788  stirlinglem6  46793  stirlinglem7  46794  stirlinglem10  46797  stirlinglem12  46799  stirlinglem13  46800  stirlingr  46804  dirkertrigeqlem1  46812  fourierdlem10  46831  fourierdlem11  46832  fourierdlem12  46833  fourierdlem14  46835  fourierdlem15  46836  fourierdlem17  46838  fourierdlem19  46840  fourierdlem30  46851  fourierdlem37  46858  fourierdlem40  46861  fourierdlem41  46862  fourierdlem42  46863  fourierdlem47  46867  fourierdlem48  46868  fourierdlem49  46869  fourierdlem50  46870  fourierdlem51  46871  fourierdlem54  46874  fourierdlem63  46883  fourierdlem64  46884  fourierdlem65  46885  fourierdlem68  46888  fourierdlem73  46893  fourierdlem74  46894  fourierdlem76  46896  fourierdlem77  46897  fourierdlem78  46898  fourierdlem79  46899  fourierdlem81  46901  fourierdlem82  46902  fourierdlem83  46903  fourierdlem92  46912  fourierdlem93  46913  fourierdlem102  46922  fourierdlem103  46923  fourierdlem104  46924  fourierdlem107  46927  fourierdlem111  46931  fourierdlem114  46934  sqwvfoura  46942  sqwvfourb  46943  fouriersw  46945  etransclem19  46967  etransclem23  46971  etransclem35  46983  etransclem41  46989  qndenserrnbllem  47008  iundjiun  47174  carageniuncllem2  47236  caratheodorylem1  47240  hoicvr  47262  ovnsubaddlem1  47284  hsphoidmvle2  47299  hoidmv1lelem1  47305  hoidmv1lelem2  47306  hoidmvlelem1  47309  hoidmvlelem2  47310  hoidmvlelem3  47311  hoiqssbllem1  47336  hoiqssbllem2  47337  volico2  47355  iinhoiicclem  47387  iunhoiioolem  47389  vonioolem2  47395  vonicclem2  47398  pimdecfgtioo  47431  pimincfltioo  47432  smflimlem4  47488  smfmullem1  47505  smflimsuplem4  47537  gpg3kgrtriexlem4  48851  gpg3kgrtriexlem6  48853  expnegico01  49298  eenglngeehlnmlem2  49518  inlinecirc02plem  49566