Theorem ltled 8074

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

Syntax hints:   → wi 4   ∈ wcel 2148   class class class wbr 4003  ℝcr 7809   < clt 7990   ≤ cle 7991

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 4121  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-cnex 7901  ax-resscn 7902  ax-pre-ltirr 7922  ax-pre-lttrn 7924

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 2739  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-opab 4065  df-xp 4632  df-cnv 4634  df-pnf 7992  df-mnf 7993  df-xr 7994  df-ltxr 7995  df-le 7996

This theorem is referenced by:  ltnsymd  8075  addgt0d  8476  lt2addd  8522  lt2msq1  8840  lediv12a  8849  ledivp1  8858  nn2ge  8950  fznatpl1  10073  exbtwnzlemex  10247  apbtwnz  10271  iseqf1olemkle  10481  expnbnd  10640  nn0ltexp2  10685  cvg1nlemres  10989  resqrexlemnm  11022  resqrexlemcvg  11023  resqrexlemglsq  11026  sqrtgt0  11038  leabs  11078  ltabs  11091  abslt  11092  absle  11093  maxabslemab  11210  2zsupmax  11229  2zinfmin  11246  xrmaxiflemab  11250  fsum3cvg3  11399  divcnv  11500  expcnvre  11506  absltap  11512  cvgratnnlemnexp  11527  cvgratnnlemmn  11528  cvgratnnlemfm  11532  mertenslemi1  11538  cos12dec  11770  dvdslelemd  11843  divalglemnn  11917  divalglemeuneg  11922  lcmgcdlem  12071  isprm5lem  12135  znege1  12172  sqrt2irraplemnn  12173  eulerthlemrprm  12223  eulerthlema  12224  4sqlem7  12376  ennnfonelemex  12409  strleund  12556  suplociccreex  13995  ivthinclemlm  14005  ivthinclemum  14006  ivthinclemlopn  14007  ivthinclemuopn  14009  ivthdec  14015  dveflem  14080  efltlemlt  14088  sin0pilem1  14095  sin0pilem2  14096  coseq0negpitopi  14150  tangtx  14152  cosq34lt1  14164  cos02pilt1  14165  apdifflemf  14676