Theorem leneltd 11381

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ≠ wne 2960   class class class wbr 5111  ℝcr 11116   < clt 11260   ≤ cle 11261

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11174  ax-pre-lttri 11191  ax-pre-lttrn 11192

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11262  df-mnf 11263  df-xr 11264  df-ltxr 11265  df-le 11266

This theorem is used by:  flltnz  13864  seqf1olem1  14097  isprm5  16790  chnccat  18706  fvmptnn04if  23058  zcld  25024  evth  25171  pmltpclem2  25661  abelthlem2  26648  cos02pilt1  26744  logcj  26824  argimgt0  26830  dvloglem  26866  logf1o2  26868  asinneg  27104  lgslem1  27514  lgseisen  27596  dchrisum0flblem1  27725  ttgcontlem1  29291  axcontlem8  29378  sgnval2  33152  unbdqndv2lem2  37158  poimirlem17  38347  aks6d1c7lem1  43007  fzdifsuc2  46089  xralrple2  46130  xralrple3  46149  eliccelioc  46297  limcresiooub  46416  limcresioolb  46417  icccncfext  46661  cncfiooiccre  46669  dvbdfbdioolem2  46703  dvnxpaek  46716  volioc  46746  itgioocnicc  46751  iblcncfioo  46752  dirkercncflem1  46877  fourierdlem24  46905  fourierdlem25  46906  fourierdlem32  46913  fourierdlem33  46914  fourierdlem41  46922  fourierdlem42  46923  fourierdlem46  46926  fourierdlem48  46928  fourierdlem49  46929  fourierdlem51  46931  fourierdlem64  46944  fourierdlem65  46945  fourierdlem73  46953  fourierdlem76  46956  fourierdlem79  46959  fourierdlem81  46961  fourierdlem82  46962  fourierdlem89  46969  fourierdlem91  46971  fourierdlem102  46982  fourierdlem114  46994  fourierswlem  47004  fouriersw  47005  etransclem15  47023  etransclem24  47032  etransclem25  47033  etransclem35  47043  iundjiun  47234  hoidmvlelem2  47370