Theorem leneltd 11304

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

Syntax hints:   → wi 4   ∈ wcel 2109   ≠ wne 2925   class class class wbr 5102  ℝcr 11043   < clt 11184   ≤ cle 11185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-pre-lttri 11118  ax-pre-lttrn 11119

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-po 5539  df-so 5540  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190

This theorem is referenced by:  flltnz  13749  seqf1olem1  13982  isprm5  16653  fvmptnn04if  22769  zcld  24735  evth  24891  pmltpclem2  25383  abelthlem2  26375  cos02pilt1  26468  logcj  26548  argimgt0  26554  dvloglem  26590  logf1o2  26592  asinneg  26829  lgslem1  27241  lgseisen  27323  dchrisum0flblem1  27452  ttgcontlem1  28865  axcontlem8  28951  sgnval2  32708  unbdqndv2lem2  36491  poimirlem17  37624  aks6d1c7lem1  42161  fzdifsuc2  45301  xralrple2  45343  xralrple3  45363  eliccelioc  45512  limcresiooub  45633  limcresioolb  45634  icccncfext  45878  cncfiooiccre  45886  dvbdfbdioolem2  45920  dvnxpaek  45933  volioc  45963  itgioocnicc  45968  iblcncfioo  45969  dirkercncflem1  46094  fourierdlem24  46122  fourierdlem25  46123  fourierdlem32  46130  fourierdlem33  46131  fourierdlem41  46139  fourierdlem42  46140  fourierdlem46  46143  fourierdlem48  46145  fourierdlem49  46146  fourierdlem51  46148  fourierdlem64  46161  fourierdlem65  46162  fourierdlem73  46170  fourierdlem76  46173  fourierdlem79  46176  fourierdlem81  46178  fourierdlem82  46179  fourierdlem89  46186  fourierdlem91  46188  fourierdlem102  46199  fourierdlem114  46211  fourierswlem  46221  fouriersw  46222  etransclem15  46240  etransclem24  46249  etransclem25  46250  etransclem35  46260  iundjiun  46451  hoidmvlelem2  46587