Theorem leneltd 11425

Description: 'Less than or equal to' and 'not equals' implies 'less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltd.2	⊢ (𝜑 → 𝐵 ∈ ℝ)
leltned.3	⊢ (𝜑 → 𝐴 ≤ 𝐵)
leneltd.4	⊢ (𝜑 → 𝐵 ≠ 𝐴)

Assertion

Ref	Expression
leneltd	⊢ (𝜑 → 𝐴 < 𝐵)

Proof of Theorem leneltd

Step	Hyp	Ref	Expression
1		leneltd.4	. 2 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
2		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
3		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4		leltned.3	. . 3 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
5	2, 3, 4	leltned 11424	. 2 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴))
6	1, 5	mpbird 256	1 ⊢ (𝜑 → 𝐴 < 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2100   ≠ wne 2933   class class class wbr 5156  ℝcr 11164   < clt 11305   ≤ cle 11306

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-sep 5307  ax-nul 5314  ax-pow 5373  ax-pr 5437  ax-un 7751  ax-resscn 11222  ax-pre-lttri 11239  ax-pre-lttrn 11240

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-rab 3429  df-v 3474  df-sbc 3789  df-csb 3905  df-dif 3962  df-un 3964  df-in 3966  df-ss 3976  df-nul 4336  df-if 4537  df-pw 4612  df-sn 4637  df-pr 4639  df-op 4643  df-uni 4919  df-br 5157  df-opab 5219  df-mpt 5240  df-id 5584  df-po 5598  df-so 5599  df-xp 5692  df-rel 5693  df-cnv 5694  df-co 5695  df-dm 5696  df-rn 5697  df-res 5698  df-ima 5699  df-iota 6510  df-fun 6560  df-fn 6561  df-f 6562  df-f1 6563  df-fo 6564  df-f1o 6565  df-fv 6566  df-er 8742  df-en 8983  df-dom 8984  df-sdom 8985  df-pnf 11307  df-mnf 11308  df-xr 11309  df-ltxr 11310  df-le 11311

This theorem is referenced by:  flltnz  13842  seqf1olem1  14072  isprm5  16729  fvmptnn04if  22865  zcld  24843  evth  24999  pmltpclem2  25492  abelthlem2  26485  cos02pilt1  26576  logcj  26656  argimgt0  26662  dvloglem  26698  logf1o2  26700  asinneg  26937  lgslem1  27349  lgseisen  27431  dchrisum0flblem1  27560  ttgcontlem1  28841  axcontlem8  28928  unbdqndv2lem2  36261  poimirlem17  37385  aks6d1c7lem1  41926  fzdifsuc2  44995  xralrple2  45039  xralrple3  45059  eliccelioc  45209  limcresiooub  45333  limcresioolb  45334  icccncfext  45578  cncfiooiccre  45586  dvbdfbdioolem2  45620  dvnxpaek  45633  volioc  45663  itgioocnicc  45668  iblcncfioo  45669  dirkercncflem1  45794  fourierdlem24  45822  fourierdlem25  45823  fourierdlem32  45830  fourierdlem33  45831  fourierdlem41  45839  fourierdlem42  45840  fourierdlem46  45843  fourierdlem48  45845  fourierdlem49  45846  fourierdlem51  45848  fourierdlem64  45861  fourierdlem65  45862  fourierdlem73  45870  fourierdlem76  45873  fourierdlem79  45876  fourierdlem81  45878  fourierdlem82  45879  fourierdlem89  45886  fourierdlem91  45888  fourierdlem102  45899  fourierdlem114  45911  fourierswlem  45921  fouriersw  45922  etransclem15  45940  etransclem24  45949  etransclem25  45950  etransclem35  45960  iundjiun  46151  hoidmvlelem2  46287