Theorem leneltd 10593

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

Syntax hints:   → wi 4   ∈ wcel 2051   ≠ wne 2962   class class class wbr 4926  ℝcr 10333   < clt 10473   ≤ cle 10474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-resscn 10391  ax-pre-lttri 10408  ax-pre-lttrn 10409

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-po 5323  df-so 5324  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-er 8088  df-en 8306  df-dom 8307  df-sdom 8308  df-pnf 10475  df-mnf 10476  df-xr 10477  df-ltxr 10478  df-le 10479

This theorem is referenced by:  flltnz  12995  seqf1olem1  13223  isprm5  15906  fvmptnn04if  21177  zcld  23140  evth  23282  pmltpclem2  23769  abelthlem2  24739  logcj  24906  argimgt0  24912  dvloglem  24948  logf1o2  24950  asinneg  25181  lgslem1  25591  lgseisen  25673  dchrisum0flblem1  25802  ttgcontlem1  26390  axcontlem8  26476  unbdqndv2lem2  33402  fzdifsuc2  41036  xralrple2  41081  xralrple3  41101  eliccelioc  41258  limcresiooub  41384  limcresioolb  41385  icccncfext  41630  cncfiooiccre  41638  dvbdfbdioolem2  41674  dvnxpaek  41687  volioc  41717  itgioocnicc  41722  iblcncfioo  41723  dirkercncflem1  41849  fourierdlem24  41877  fourierdlem25  41878  fourierdlem32  41885  fourierdlem33  41886  fourierdlem41  41894  fourierdlem42  41895  fourierdlem46  41898  fourierdlem48  41900  fourierdlem49  41901  fourierdlem51  41903  fourierdlem64  41916  fourierdlem65  41917  fourierdlem73  41925  fourierdlem76  41928  fourierdlem79  41931  fourierdlem81  41933  fourierdlem82  41934  fourierdlem89  41941  fourierdlem91  41943  fourierdlem102  41954  fourierdlem114  41966  fourierswlem  41976  fouriersw  41977  etransclem15  41995  etransclem24  42004  etransclem25  42005  etransclem35  42015  iundjiun  42203  hoidmvlelem2  42339