Theorem ltled 7994

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

Hypotheses

Ref	Expression
ltd.1	|- ( ph -> A e. RR )
ltd.2	|- ( ph -> B e. RR )
ltled.1	|- ( ph -> A < B )

Assertion

Ref	Expression
ltled	|- ( ph -> A <_ B )

Proof of Theorem ltled

Step	Hyp	Ref	Expression
1		ltled.1	. 2 |- ( ph -> A < B )
2		ltd.1	. . 3 |- ( ph -> A e. RR )
3		ltd.2	. . 3 |- ( ph -> B e. RR )
4		ltle 7964	. . 3 |- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )
5	2, 3, 4	syl2anc 409	. 2 |- ( ph -> ( A < B -> A <_ B ) )
6	1, 5	mpd 13	1 |- ( ph -> A <_ B )

Syntax hints:   -> wi 4   e. wcel 2128   class class class wbr 3965   RRcr 7731   < clt 7912   <_ cle 7913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4496  ax-cnex 7823  ax-resscn 7824  ax-pre-ltirr 7844  ax-pre-lttrn 7846

This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1338  df-fal 1341  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-rab 2444  df-v 2714  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-br 3966  df-opab 4026  df-xp 4592  df-cnv 4594  df-pnf 7914  df-mnf 7915  df-xr 7916  df-ltxr 7917  df-le 7918

This theorem is referenced by:  ltnsymd  7995  addgt0d  8396  lt2addd  8442  lt2msq1  8756  lediv12a  8765  ledivp1  8774  nn2ge  8866  fznatpl1  9978  exbtwnzlemex  10149  apbtwnz  10173  iseqf1olemkle  10383  expnbnd  10541  cvg1nlemres  10885  resqrexlemnm  10918  resqrexlemcvg  10919  resqrexlemglsq  10922  sqrtgt0  10934  leabs  10974  ltabs  10987  abslt  10988  absle  10989  maxabslemab  11106  2zsupmax  11125  xrmaxiflemab  11144  fsum3cvg3  11293  divcnv  11394  expcnvre  11400  absltap  11406  cvgratnnlemnexp  11421  cvgratnnlemmn  11422  cvgratnnlemfm  11426  mertenslemi1  11432  cos12dec  11664  dvdslelemd  11734  divalglemnn  11808  divalglemeuneg  11813  lcmgcdlem  11953  znege1  12052  sqrt2irraplemnn  12053  eulerthlemrprm  12103  eulerthlema  12104  ennnfonelemex  12143  strleund  12278  suplociccreex  13002  ivthinclemlm  13012  ivthinclemum  13013  ivthinclemlopn  13014  ivthinclemuopn  13016  ivthdec  13022  dveflem  13087  efltlemlt  13095  sin0pilem1  13102  sin0pilem2  13103  coseq0negpitopi  13157  tangtx  13159  cosq34lt1  13171  cos02pilt1  13172  apdifflemf  13617