Theorem ltled 8288

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

Syntax hints:   → wi 4   ∈ wcel 2200   class class class wbr 4086  ℝcr 8021   < clt 8204   ≤ cle 8205

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 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-cnex 8113  ax-resscn 8114  ax-pre-ltirr 8134  ax-pre-lttrn 8136

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 2802  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-xp 4729  df-cnv 4731  df-pnf 8206  df-mnf 8207  df-xr 8208  df-ltxr 8209  df-le 8210

This theorem is referenced by:  ltnsymd  8289  addgt0d  8691  lt2addd  8737  lt2msq1  9055  lediv12a  9064  ledivp1  9073  nn2ge  9166  fznatpl1  10301  exbtwnzlemex  10499  apbtwnz  10524  iseqf1olemkle  10749  expnbnd  10915  nn0ltexp2  10961  iswrdiz  11110  cvg1nlemres  11536  resqrexlemnm  11569  resqrexlemcvg  11570  resqrexlemglsq  11573  sqrtgt0  11585  leabs  11625  ltabs  11638  abslt  11639  absle  11640  maxabslemab  11757  2zsupmax  11777  2zinfmin  11794  xrmaxiflemab  11798  fsum3cvg3  11947  divcnv  12048  expcnvre  12054  absltap  12060  cvgratnnlemnexp  12075  cvgratnnlemmn  12076  cvgratnnlemfm  12080  mertenslemi1  12086  sinltxirr  12312  cos12dec  12319  dvdslelemd  12394  divalglemnn  12469  divalglemeuneg  12474  bitsfzo  12506  bitsmod  12507  lcmgcdlem  12639  isprm5lem  12703  znege1  12740  sqrt2irraplemnn  12741  eulerthlemrprm  12791  eulerthlema  12792  4sqlem7  12947  ennnfonelemex  13025  strleund  13176  suplociccreex  15338  ivthinclemlm  15348  ivthinclemum  15349  ivthinclemlopn  15350  ivthinclemuopn  15352  ivthdec  15358  hoverlt1  15363  hovergt0  15364  dveflem  15440  efltlemlt  15488  sin0pilem1  15495  sin0pilem2  15496  coseq0negpitopi  15550  tangtx  15552  cosq34lt1  15564  cos02pilt1  15565  lgseisenlem1  15789  lgsquadlem1  15796  lgsquadlem2  15797  lgsquadlem3  15798  apdifflemf  16586