Theorem ltned 9797

Description: 'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.)

Hypotheses

Ref	Expression
ltd.1	|- ( ph -> A e. RR )
ltned.2	|- ( ph -> A < B )

Assertion

Ref	Expression
ltned	|- ( ph -> A =/= B )

Proof of Theorem ltned

Step	Hyp	Ref	Expression
1		ltd.1	. . 3 |- ( ph -> A e. RR )
2		ltned.2	. . 3 |- ( ph -> A < B )
3	1, 2	gtned 9796	. 2 |- ( ph -> B =/= A )
4	3	necomd 2691	1 |- ( ph -> A =/= B )

Syntax hints:   -> wi 4   e. wcel 1898   =/= wne 2633   class class class wbr 4416   RRcr 9564   < clt 9701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-resscn 9622  ax-pre-lttri 9639  ax-pre-lttrn 9640

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-mpt 4477  df-id 4768  df-po 4774  df-so 4775  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-pnf 9703  df-mnf 9704  df-ltxr 9706

This theorem is referenced by:  seqf1olem1  12284  nprm  14687  4sqlem10  14940  4sqlem17OLD  14954  4sqlem17  14960  pgpfaclem2  17764  fvmptnn04ifb  19924  dvferm2lem  22987  lhop2  23016  ftc1lem5  23041  deg1tmle  23115  plyeq0lem  23213  aaliou3lem7  23354  dvloglem  23642  isosctrlem1  23796  bndatandm  23904  vma1  24142  rplogsumlem2  24372  rpvmasumlem  24374  axlowdimlem13  25033  axlowdimlem16  25036  nbhashuvtx1  25692  strlem6  27958  hstrlem6  27966  pmtrto1cl  28661  psgnfzto1stlem  28662  1smat1  28679  submateqlem1  28682  submateqlem2  28683  madjusmdetlem2  28703  xrge0iifcnv  28788  erdszelem8  29970  ivthALT  31040  poimirlem1  31986  poimirlem6  31991  poimirlem7  31992  poimirlem9  31994  poimirlem15  32000  poimirlem22  32007  radcnvrat  36707  isosctrlem1ALT  37371  lptre2pt  37758  cncfiooicclem1  37809  cncfioobdlem  37812  ditgeqiooicc  37875  itgioocnicc  37892  iblcncfioo  37893  stirlinglem7  37980  fourierdlem34  38042  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem54  38062  fourierdlem60  38068  fourierdlem73  38081  fourierdlem74  38082  fourierdlem76  38084  fourierdlem81  38089  fourierdlem82  38090  fourierdlem84  38092  fourierdlem93  38101  fourierdlem103  38111  fourierdlem104  38112  fourierdlem111  38119  fourierswlem  38132