Theorem ltned 11347

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

Syntax hints:   → wi 4   ∈ wcel 2107   ≠ wne 2941   class class class wbr 5148  ℝcr 11106   < clt 11245

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-resscn 11164  ax-pre-lttri 11181  ax-pre-lttrn 11182

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-er 8700  df-en 8937  df-dom 8938  df-sdom 8939  df-pnf 11247  df-mnf 11248  df-ltxr 11250

This theorem is referenced by:  fzodisjsn  13667  modsumfzodifsn  13906  seqf1olem1  14004  nprm  16622  4sqlem10  16877  4sqlem17  16891  pgpfaclem2  19947  fvmptnn04ifb  22345  dvferm2lem  25495  lhop2  25524  ftc1lem5  25549  deg1tmle  25627  plyeq0lem  25716  aaliou3lem7  25854  dvloglem  26148  isosctrlem1  26313  bndatandm  26424  vma1  26660  rplogsumlem2  26978  rpvmasumlem  26980  axlowdimlem13  28202  axlowdimlem16  28205  strlem6  31497  hstrlem6  31505  fzone1  31999  pmtrto1cl  32246  psgnfzto1stlem  32247  cycpmrn  32290  drngidlhash  32541  prmidl0  32558  krull  32583  1smat1  32773  submateqlem1  32776  submateqlem2  32777  madjusmdetlem2  32797  xrge0iifcnv  32902  reprlt  33620  reprgt  33622  reprinfz1  33623  erdszelem8  34178  ivthALT  35209  knoppndvlem1  35377  knoppndvlem2  35378  knoppndvlem7  35383  knoppndvlem21  35397  irrdiff  36196  poimirlem1  36478  poimirlem6  36483  poimirlem7  36484  poimirlem9  36486  poimirlem15  36492  poimirlem22  36499  3lexlogpow5ineq1  40908  3lexlogpow5ineq2  40909  3lexlogpow5ineq4  40910  3lexlogpow5ineq3  40911  3lexlogpow2ineq1  40912  3lexlogpow2ineq2  40913  3lexlogpow5ineq5  40914  aks4d1lem1  40916  dvrelog2b  40920  0nonelalab  40921  dvrelogpow2b  40922  aks4d1p1p3  40923  aks4d1p1p2  40924  aks4d1p1p4  40925  aks4d1p1p6  40927  aks4d1p1p7  40928  aks4d1p1p5  40929  aks4d1p1  40930  aks4d1p2  40931  aks4d1p3  40932  aks4d1p5  40934  aks4d1p6  40935  aks4d1p7d1  40936  aks4d1p7  40937  aks4d1p8d3  40940  aks4d1p8  40941  aks4d1p9  40942  aks6d1c2p2  40946  2np3bcnp1  40949  2ap1caineq  40950  sticksstones1  40951  sticksstones2  40952  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  sticksstones22  40973  metakunt6  40979  metakunt7  40980  metakunt11  40984  metakunt12  40985  metakunt27  41000  metakunt28  41001  metakunt29  41002  metakunt30  41003  rtprmirr  41234  sn-0ne2  41276  radcnvrat  43059  isosctrlem1ALT  43681  ltdiv23neg  44091  lptre2pt  44343  cncfiooicclem1  44596  cncfioobdlem  44599  ditgeqiooicc  44663  itgioocnicc  44680  iblcncfioo  44681  stirlinglem7  44783  fourierdlem34  44844  fourierdlem42  44852  fourierdlem54  44863  fourierdlem60  44869  fourierdlem73  44882  fourierdlem74  44883  fourierdlem76  44885  fourierdlem81  44890  fourierdlem82  44891  fourierdlem84  44893  fourierdlem93  44902  fourierdlem103  44912  fourierdlem104  44913  fourierdlem111  44920  fourierswlem  44933  pimrecltneg  45427  eenglngeehlnmlem2  47378