Theorem ltled 8265

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 8234	. . 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 2200   class class class wbr 4083   RRcr 7998   < clt 8181   <_ cle 8182

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8090  ax-resscn 8091  ax-pre-ltirr 8111  ax-pre-lttrn 8113

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-xp 4725  df-cnv 4727  df-pnf 8183  df-mnf 8184  df-xr 8185  df-ltxr 8186  df-le 8187

This theorem is referenced by:  ltnsymd  8266  addgt0d  8668  lt2addd  8714  lt2msq1  9032  lediv12a  9041  ledivp1  9050  nn2ge  9143  fznatpl1  10272  exbtwnzlemex  10469  apbtwnz  10494  iseqf1olemkle  10719  expnbnd  10885  nn0ltexp2  10931  iswrdiz  11078  cvg1nlemres  11496  resqrexlemnm  11529  resqrexlemcvg  11530  resqrexlemglsq  11533  sqrtgt0  11545  leabs  11585  ltabs  11598  abslt  11599  absle  11600  maxabslemab  11717  2zsupmax  11737  2zinfmin  11754  xrmaxiflemab  11758  fsum3cvg3  11907  divcnv  12008  expcnvre  12014  absltap  12020  cvgratnnlemnexp  12035  cvgratnnlemmn  12036  cvgratnnlemfm  12040  mertenslemi1  12046  sinltxirr  12272  cos12dec  12279  dvdslelemd  12354  divalglemnn  12429  divalglemeuneg  12434  bitsfzo  12466  bitsmod  12467  lcmgcdlem  12599  isprm5lem  12663  znege1  12700  sqrt2irraplemnn  12701  eulerthlemrprm  12751  eulerthlema  12752  4sqlem7  12907  ennnfonelemex  12985  strleund  13136  suplociccreex  15298  ivthinclemlm  15308  ivthinclemum  15309  ivthinclemlopn  15310  ivthinclemuopn  15312  ivthdec  15318  hoverlt1  15323  hovergt0  15324  dveflem  15400  efltlemlt  15448  sin0pilem1  15455  sin0pilem2  15456  coseq0negpitopi  15510  tangtx  15512  cosq34lt1  15524  cos02pilt1  15525  lgseisenlem1  15749  lgsquadlem1  15756  lgsquadlem2  15757  lgsquadlem3  15758  apdifflemf  16414