Theorem ltned 11371

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ≠ wne 2955   class class class wbr 5103  ℝcr 11124   < clt 11268

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pow 5330  ax-pr 5398  ax-un 7737  ax-resscn 11182  ax-pre-lttri 11199  ax-pre-lttrn 11200

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-po 5563  df-so 5564  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-er 8697  df-en 8954  df-dom 8955  df-sdom 8956  df-pnf 11270  df-mnf 11271  df-ltxr 11273

This theorem is used by:  fzodisjsn  13754  fzone1  13841  modsumfzodifsn  14009  seqf1olem1  14106  nprm  16779  4sqlem10  17040  4sqlem17  17054  pgpfaclem2  20212  prmidl0  21542  fvmptnn04ifb  23077  dvferm2lem  26214  lhop2  26243  ftc1lem5  26268  deg1tmle  26344  plyeq0lem  26437  aaliou3lem7  26586  dvloglem  26886  rtprmirr  26998  isosctrlem1  27056  bndatandm  27167  vma1  27403  rplogsumlem2  27722  rpvmasumlem  27724  axlowdimlem13  29412  axlowdimlem16  29415  strlem6  32738  hstrlem6  32746  pmtrto1cl  33540  psgnfzto1stlem  33541  cycpmrn  33584  drngidlhash  33862  krull  33882  esplyfval2  34076  esplyfval3  34083  cos9thpiminply  34299  1smat1  34315  submateqlem1  34318  submateqlem2  34319  xrge0iifcnv  34444  reprlt  35128  reprgt  35130  reprinfz1  35131  erdszelem8  35778  ivthALT  36955  knoppndvlem1  37210  knoppndvlem2  37211  knoppndvlem7  37216  knoppndvlem21  37230  irrdiff  38079  qdiff  38080  poimirlem1  38371  poimirlem6  38376  poimirlem7  38377  poimirlem9  38379  poimirlem15  38385  poimirlem22  38392  3lexlogpow5ineq1  42921  3lexlogpow5ineq2  42922  3lexlogpow5ineq4  42923  3lexlogpow5ineq3  42924  3lexlogpow2ineq1  42925  3lexlogpow2ineq2  42926  3lexlogpow5ineq5  42927  aks4d1lem1  42929  dvrelog2b  42933  0nonelalab  42934  dvrelogpow2b  42935  aks4d1p1p3  42936  aks4d1p1p2  42937  aks4d1p1p4  42938  aks4d1p1p6  42940  aks4d1p1p7  42941  aks4d1p1p5  42942  aks4d1p1  42943  aks4d1p2  42944  aks4d1p3  42945  aks4d1p5  42947  aks4d1p6  42948  aks4d1p7d1  42949  aks4d1p7  42950  aks4d1p8d3  42953  aks4d1p8  42954  aks4d1p9  42955  aks6d1c2p2  42986  aks6d1c3  42990  2np3bcnp1  43011  2ap1caineq  43012  sticksstones1  43013  sticksstones2  43014  sticksstones10  43022  sticksstones12a  43024  sticksstones12  43025  sticksstones22  43035  aks6d1c6lem4  43040  aks6d1c7lem2  43048  aks5lem8  43068  sn-0ne2  43282  radcnvrat  45139  isosctrlem1ALT  45757  ltdiv23neg  46224  lptre2pt  46469  cncfiooicclem1  46722  cncfioobdlem  46725  ditgeqiooicc  46789  itgioocnicc  46806  iblcncfioo  46807  stirlinglem7  46909  fourierdlem34  46970  fourierdlem42  46978  fourierdlem54  46989  fourierdlem60  46995  fourierdlem73  47008  fourierdlem74  47009  fourierdlem76  47011  fourierdlem81  47016  fourierdlem82  47017  fourierdlem84  47019  fourierdlem93  47028  fourierdlem103  47038  fourierdlem104  47039  fourierdlem111  47046  fourierswlem  47059  pimrecltneg  47553  upgrimpthslem2  48825  stgrusgra  48876  eenglngeehlnmlem2  49669