Theorem ltled 8138

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 8107	. . 3 |- ( ( A e. RR /\ B e. RR ) -> ( A < B -> A <_ B ) )
5	2, 3, 4	syl2anc 411	. 2 |- ( ph -> ( A < B -> A <_ B ) )
6	1, 5	mpd 13	1 |- ( ph -> A <_ B )

Syntax hints:   -> wi 4   e. wcel 2164   class class class wbr 4029   RRcr 7871   < clt 8054   <_ cle 8055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-pre-ltirr 7984  ax-pre-lttrn 7986

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-xp 4665  df-cnv 4667  df-pnf 8056  df-mnf 8057  df-xr 8058  df-ltxr 8059  df-le 8060

This theorem is referenced by:  ltnsymd  8139  addgt0d  8540  lt2addd  8586  lt2msq1  8904  lediv12a  8913  ledivp1  8922  nn2ge  9015  fznatpl1  10142  exbtwnzlemex  10318  apbtwnz  10343  iseqf1olemkle  10568  expnbnd  10734  nn0ltexp2  10780  iswrdiz  10921  cvg1nlemres  11129  resqrexlemnm  11162  resqrexlemcvg  11163  resqrexlemglsq  11166  sqrtgt0  11178  leabs  11218  ltabs  11231  abslt  11232  absle  11233  maxabslemab  11350  2zsupmax  11369  2zinfmin  11386  xrmaxiflemab  11390  fsum3cvg3  11539  divcnv  11640  expcnvre  11646  absltap  11652  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratnnlemfm  11672  mertenslemi1  11678  sinltxirr  11904  cos12dec  11911  dvdslelemd  11985  divalglemnn  12059  divalglemeuneg  12064  lcmgcdlem  12215  isprm5lem  12279  znege1  12316  sqrt2irraplemnn  12317  eulerthlemrprm  12367  eulerthlema  12368  4sqlem7  12522  ennnfonelemex  12571  strleund  12721  suplociccreex  14778  ivthinclemlm  14788  ivthinclemum  14789  ivthinclemlopn  14790  ivthinclemuopn  14792  ivthdec  14798  hoverlt1  14803  hovergt0  14804  dveflem  14872  efltlemlt  14909  sin0pilem1  14916  sin0pilem2  14917  coseq0negpitopi  14971  tangtx  14973  cosq34lt1  14985  cos02pilt1  14986  lgseisenlem1  15186  lgsquadlem1  15191  apdifflemf  15536