Theorem ltned 11111

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 11110	. 2 ⊢ (𝜑 → 𝐵 ≠ 𝐴)
4	3	necomd 2999	1 ⊢ (𝜑 → 𝐴 ≠ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2106   ≠ wne 2943   class class class wbr 5074  ℝcr 10870   < clt 11009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588  ax-resscn 10928  ax-pre-lttri 10945  ax-pre-lttrn 10946

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-po 5503  df-so 5504  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-er 8498  df-en 8734  df-dom 8735  df-sdom 8736  df-pnf 11011  df-mnf 11012  df-ltxr 11014

This theorem is referenced by:  fzodisjsn  13425  modsumfzodifsn  13664  seqf1olem1  13762  nprm  16393  4sqlem10  16648  4sqlem17  16662  pgpfaclem2  19685  fvmptnn04ifb  22000  dvferm2lem  25150  lhop2  25179  ftc1lem5  25204  deg1tmle  25282  plyeq0lem  25371  aaliou3lem7  25509  dvloglem  25803  isosctrlem1  25968  bndatandm  26079  vma1  26315  rplogsumlem2  26633  rpvmasumlem  26635  axlowdimlem13  27322  axlowdimlem16  27325  strlem6  30618  hstrlem6  30626  fzone1  31121  pmtrto1cl  31366  psgnfzto1stlem  31367  cycpmrn  31410  prmidl0  31626  krull  31643  1smat1  31754  submateqlem1  31757  submateqlem2  31758  madjusmdetlem2  31778  xrge0iifcnv  31883  reprlt  32599  reprgt  32601  reprinfz1  32602  erdszelem8  33160  ivthALT  34524  knoppndvlem1  34692  knoppndvlem2  34693  knoppndvlem7  34698  knoppndvlem21  34712  irrdiff  35497  poimirlem1  35778  poimirlem6  35783  poimirlem7  35784  poimirlem9  35786  poimirlem15  35792  poimirlem22  35799  3lexlogpow5ineq1  40062  3lexlogpow5ineq2  40063  3lexlogpow5ineq4  40064  3lexlogpow5ineq3  40065  3lexlogpow2ineq1  40066  3lexlogpow2ineq2  40067  3lexlogpow5ineq5  40068  aks4d1lem1  40070  dvrelog2b  40074  0nonelalab  40075  dvrelogpow2b  40076  aks4d1p1p3  40077  aks4d1p1p2  40078  aks4d1p1p4  40079  aks4d1p1p6  40081  aks4d1p1p7  40082  aks4d1p1p5  40083  aks4d1p1  40084  aks4d1p2  40085  aks4d1p3  40086  aks4d1p5  40088  aks4d1p6  40089  aks4d1p7d1  40090  aks4d1p7  40091  aks4d1p8d3  40094  aks4d1p8  40095  aks4d1p9  40096  2np3bcnp1  40100  2ap1caineq  40101  sticksstones1  40102  sticksstones2  40103  sticksstones10  40111  sticksstones12a  40113  sticksstones12  40114  sticksstones22  40124  metakunt6  40130  metakunt7  40131  metakunt11  40135  metakunt12  40136  metakunt27  40151  metakunt28  40152  metakunt29  40153  metakunt30  40154  rtprmirr  40347  sn-0ne2  40389  radcnvrat  41932  isosctrlem1ALT  42554  ltdiv23neg  42934  lptre2pt  43181  cncfiooicclem1  43434  cncfioobdlem  43437  ditgeqiooicc  43501  itgioocnicc  43518  iblcncfioo  43519  stirlinglem7  43621  fourierdlem34  43682  fourierdlem42  43690  fourierdlem54  43701  fourierdlem60  43707  fourierdlem73  43720  fourierdlem74  43721  fourierdlem76  43723  fourierdlem81  43728  fourierdlem82  43729  fourierdlem84  43731  fourierdlem93  43740  fourierdlem103  43750  fourierdlem104  43751  fourierdlem111  43758  fourierswlem  43771  pimrecltneg  44260  eenglngeehlnmlem2  46084