Theorem leneltd 11285

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 11284	. 2 ⊢ (𝜑 → (𝐴 < 𝐵 ↔ 𝐵 ≠ 𝐴))
6	1, 5	mpbird 257	1 ⊢ (𝜑 → 𝐴 < 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2113   ≠ wne 2930   class class class wbr 5096  ℝcr 11023   < clt 11164   ≤ cle 11165

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-resscn 11081  ax-pre-lttri 11098  ax-pre-lttrn 11099

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-er 8633  df-en 8882  df-dom 8883  df-sdom 8884  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170

This theorem is referenced by:  flltnz  13729  seqf1olem1  13962  isprm5  16632  chnccat  18547  fvmptnn04if  22791  zcld  24756  evth  24912  pmltpclem2  25404  abelthlem2  26396  cos02pilt1  26489  logcj  26569  argimgt0  26575  dvloglem  26611  logf1o2  26613  asinneg  26850  lgslem1  27262  lgseisen  27344  dchrisum0flblem1  27473  ttgcontlem1  28906  axcontlem8  28993  sgnval2  32763  unbdqndv2lem2  36653  poimirlem17  37777  aks6d1c7lem1  42373  fzdifsuc2  45500  xralrple2  45541  xralrple3  45560  eliccelioc  45709  limcresiooub  45828  limcresioolb  45829  icccncfext  46073  cncfiooiccre  46081  dvbdfbdioolem2  46115  dvnxpaek  46128  volioc  46158  itgioocnicc  46163  iblcncfioo  46164  dirkercncflem1  46289  fourierdlem24  46317  fourierdlem25  46318  fourierdlem32  46325  fourierdlem33  46326  fourierdlem41  46334  fourierdlem42  46335  fourierdlem46  46338  fourierdlem48  46340  fourierdlem49  46341  fourierdlem51  46343  fourierdlem64  46356  fourierdlem65  46357  fourierdlem73  46365  fourierdlem76  46368  fourierdlem79  46371  fourierdlem81  46373  fourierdlem82  46374  fourierdlem89  46381  fourierdlem91  46383  fourierdlem102  46394  fourierdlem114  46406  fourierswlem  46416  fouriersw  46417  etransclem15  46435  etransclem24  46444  etransclem25  46445  etransclem35  46455  iundjiun  46646  hoidmvlelem2  46782