Theorem ltled 8079

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 8048	. . 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 2148   class class class wbr 4005   RRcr 7813   < clt 7995   <_ cle 7996

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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-setind 4538  ax-cnex 7905  ax-resscn 7906  ax-pre-ltirr 7926  ax-pre-lttrn 7928

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2741  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-br 4006  df-opab 4067  df-xp 4634  df-cnv 4636  df-pnf 7997  df-mnf 7998  df-xr 7999  df-ltxr 8000  df-le 8001

This theorem is referenced by:  ltnsymd  8080  addgt0d  8481  lt2addd  8527  lt2msq1  8845  lediv12a  8854  ledivp1  8863  nn2ge  8955  fznatpl1  10079  exbtwnzlemex  10253  apbtwnz  10277  iseqf1olemkle  10487  expnbnd  10647  nn0ltexp2  10692  cvg1nlemres  10997  resqrexlemnm  11030  resqrexlemcvg  11031  resqrexlemglsq  11034  sqrtgt0  11046  leabs  11086  ltabs  11099  abslt  11100  absle  11101  maxabslemab  11218  2zsupmax  11237  2zinfmin  11254  xrmaxiflemab  11258  fsum3cvg3  11407  divcnv  11508  expcnvre  11514  absltap  11520  cvgratnnlemnexp  11535  cvgratnnlemmn  11536  cvgratnnlemfm  11540  mertenslemi1  11546  cos12dec  11778  dvdslelemd  11852  divalglemnn  11926  divalglemeuneg  11931  lcmgcdlem  12080  isprm5lem  12144  znege1  12181  sqrt2irraplemnn  12182  eulerthlemrprm  12232  eulerthlema  12233  4sqlem7  12385  ennnfonelemex  12418  strleund  12565  suplociccreex  14242  ivthinclemlm  14252  ivthinclemum  14253  ivthinclemlopn  14254  ivthinclemuopn  14256  ivthdec  14262  dveflem  14327  efltlemlt  14335  sin0pilem1  14342  sin0pilem2  14343  coseq0negpitopi  14397  tangtx  14399  cosq34lt1  14411  cos02pilt1  14412  lgseisenlem1  14590  apdifflemf  14934