Theorem ltled 8298

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 8267	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
5	2, 3, 4	syl2anc 411	. 2 ⊢ (𝜑 → (𝐴 < 𝐵 → 𝐴 ≤ 𝐵))
6	1, 5	mpd 13	1 ⊢ (𝜑 → 𝐴 ≤ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2202   class class class wbr 4088  ℝcr 8031   < clt 8214   ≤ cle 8215

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 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4207  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-cnex 8123  ax-resscn 8124  ax-pre-ltirr 8144  ax-pre-lttrn 8146

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-rab 2519  df-v 2804  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-opab 4151  df-xp 4731  df-cnv 4733  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220

This theorem is referenced by:  ltnsymd  8299  addgt0d  8701  lt2addd  8747  lt2msq1  9065  lediv12a  9074  ledivp1  9083  nn2ge  9176  fznatpl1  10311  exbtwnzlemex  10509  apbtwnz  10534  iseqf1olemkle  10759  expnbnd  10925  nn0ltexp2  10971  iswrdiz  11120  cvg1nlemres  11546  resqrexlemnm  11579  resqrexlemcvg  11580  resqrexlemglsq  11583  sqrtgt0  11595  leabs  11635  ltabs  11648  abslt  11649  absle  11650  maxabslemab  11767  2zsupmax  11787  2zinfmin  11804  xrmaxiflemab  11808  fsum3cvg3  11958  divcnv  12059  expcnvre  12065  absltap  12071  cvgratnnlemnexp  12086  cvgratnnlemmn  12087  cvgratnnlemfm  12091  mertenslemi1  12097  sinltxirr  12323  cos12dec  12330  dvdslelemd  12405  divalglemnn  12480  divalglemeuneg  12485  bitsfzo  12517  bitsmod  12518  lcmgcdlem  12650  isprm5lem  12714  znege1  12751  sqrt2irraplemnn  12752  eulerthlemrprm  12802  eulerthlema  12803  4sqlem7  12958  ennnfonelemex  13036  strleund  13187  suplociccreex  15350  ivthinclemlm  15360  ivthinclemum  15361  ivthinclemlopn  15362  ivthinclemuopn  15364  ivthdec  15370  hoverlt1  15375  hovergt0  15376  dveflem  15452  efltlemlt  15500  sin0pilem1  15507  sin0pilem2  15508  coseq0negpitopi  15562  tangtx  15564  cosq34lt1  15576  cos02pilt1  15577  lgseisenlem1  15801  lgsquadlem1  15808  lgsquadlem2  15809  lgsquadlem3  15810  apdifflemf  16653