Theorem ltned 10052

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

Hypotheses

Ref	Expression
ltd.1	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltned.2	⊢ (𝜑 → 𝐴 < 𝐵)

Assertion

Ref	Expression
ltned	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Proof of Theorem ltned

Step	Hyp	Ref	Expression
1		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
2		ltned.2	. . 3 ⊢ (𝜑 → 𝐴 < 𝐵)
3	1, 2	gtned 10051	. 2 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
4	3	necomd 2837	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 1977   ≠ wne 2780   class class class wbr 4583  ℝcr 9814   < clt 9953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-pre-lttri 9889  ax-pre-lttrn 9890

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-po 4959  df-so 4960  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-ltxr 9958

This theorem is referenced by:  fzodisjsn  12374  modsumfzodifsn  12605  seqf1olem1  12702  nprm  15239  4sqlem10  15489  4sqlem17  15503  pgpfaclem2  18304  fvmptnn04ifb  20475  dvferm2lem  23553  lhop2  23582  ftc1lem5  23607  deg1tmle  23681  plyeq0lem  23770  aaliou3lem7  23908  dvloglem  24194  isosctrlem1  24348  bndatandm  24456  vma1  24692  rplogsumlem2  24974  rpvmasumlem  24976  axlowdimlem13  25634  axlowdimlem16  25637  nbhashuvtx1  26442  strlem6  28499  hstrlem6  28507  pmtrto1cl  29180  psgnfzto1stlem  29181  1smat1  29198  submateqlem1  29201  submateqlem2  29202  madjusmdetlem2  29222  xrge0iifcnv  29307  erdszelem8  30434  ivthALT  31500  knoppndvlem1  31673  knoppndvlem2  31674  knoppndvlem7  31679  knoppndvlem21  31693  poimirlem1  32580  poimirlem6  32585  poimirlem7  32586  poimirlem9  32588  poimirlem15  32594  poimirlem22  32601  radcnvrat  37535  isosctrlem1ALT  38192  ltdiv23neg  38558  lptre2pt  38707  cncfiooicclem1  38779  cncfioobdlem  38782  ditgeqiooicc  38852  itgioocnicc  38869  iblcncfioo  38870  stirlinglem7  38973  fourierdlem34  39034  fourierdlem42  39042  fourierdlem54  39053  fourierdlem60  39059  fourierdlem73  39072  fourierdlem74  39073  fourierdlem76  39075  fourierdlem81  39080  fourierdlem82  39081  fourierdlem84  39083  fourierdlem93  39092  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierswlem  39123  pimrecltneg  39610