Theorem ltned 11016

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

Syntax hints:   → wi 4   ∈ wcel 2112   ≠ wne 2943   class class class wbr 5070  ℝcr 10776   < clt 10915

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pow 5282  ax-pr 5346  ax-un 7563  ax-resscn 10834  ax-pre-lttri 10851  ax-pre-lttrn 10852

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-sbc 3713  df-csb 3830  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5153  df-id 5479  df-po 5493  df-so 5494  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-iota 6373  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-fv 6423  df-er 8433  df-en 8669  df-dom 8670  df-sdom 8671  df-pnf 10917  df-mnf 10918  df-ltxr 10920

This theorem is referenced by:  fzodisjsn  13328  modsumfzodifsn  13567  seqf1olem1  13665  nprm  16296  4sqlem10  16551  4sqlem17  16565  pgpfaclem2  19575  fvmptnn04ifb  21883  dvferm2lem  25030  lhop2  25059  ftc1lem5  25084  deg1tmle  25162  plyeq0lem  25251  aaliou3lem7  25389  dvloglem  25683  isosctrlem1  25848  bndatandm  25959  vma1  26195  rplogsumlem2  26513  rpvmasumlem  26515  axlowdimlem13  27200  axlowdimlem16  27203  strlem6  30494  hstrlem6  30502  fzone1  30998  pmtrto1cl  31243  psgnfzto1stlem  31244  cycpmrn  31287  prmidl0  31503  krull  31520  1smat1  31631  submateqlem1  31634  submateqlem2  31635  madjusmdetlem2  31655  xrge0iifcnv  31760  reprlt  32474  reprgt  32476  reprinfz1  32477  erdszelem8  33035  ivthALT  34426  knoppndvlem1  34594  knoppndvlem2  34595  knoppndvlem7  34600  knoppndvlem21  34614  irrdiff  35400  poimirlem1  35684  poimirlem6  35689  poimirlem7  35690  poimirlem9  35692  poimirlem15  35698  poimirlem22  35705  3lexlogpow5ineq1  39969  3lexlogpow5ineq2  39970  3lexlogpow5ineq4  39971  3lexlogpow5ineq3  39972  3lexlogpow2ineq1  39973  3lexlogpow2ineq2  39974  3lexlogpow5ineq5  39975  dvrelog2b  39980  0nonelalab  39981  dvrelogpow2b  39982  aks4d1p1p3  39983  aks4d1p1p2  39984  aks4d1p1p4  39985  aks4d1p1p6  39987  aks4d1p1p7  39988  aks4d1p1p5  39989  aks4d1p1  39990  aks4d1p2  39991  aks4d1p3  39992  aks4d1p5  39994  aks4d1p6  39995  aks4d1p7d1  39996  aks4d1p7  39997  2np3bcnp1  40000  2ap1caineq  40001  sticksstones1  40002  sticksstones2  40003  sticksstones10  40011  sticksstones12a  40013  sticksstones12  40014  sticksstones22  40024  metakunt6  40030  metakunt7  40031  metakunt11  40035  metakunt12  40036  metakunt27  40051  metakunt28  40052  metakunt29  40053  metakunt30  40054  rtprmirr  40240  sn-0ne2  40282  radcnvrat  41794  isosctrlem1ALT  42416  ltdiv23neg  42797  lptre2pt  43044  cncfiooicclem1  43297  cncfioobdlem  43300  ditgeqiooicc  43364  itgioocnicc  43381  iblcncfioo  43382  stirlinglem7  43484  fourierdlem34  43545  fourierdlem42  43553  fourierdlem54  43564  fourierdlem60  43570  fourierdlem73  43583  fourierdlem74  43584  fourierdlem76  43586  fourierdlem81  43591  fourierdlem82  43592  fourierdlem84  43594  fourierdlem93  43603  fourierdlem103  43613  fourierdlem104  43614  fourierdlem111  43621  fourierswlem  43634  pimrecltneg  44120  eenglngeehlnmlem2  45945