Theorem ltned 11364

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ≠ wne 2961   class class class wbr 5114  ℝcr 11117   < clt 11261

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 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-resscn 11175  ax-pre-lttri 11192  ax-pre-lttrn 11193

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 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5561  df-po 5574  df-so 5575  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-ltxr 11266

This theorem is used by:  fzodisjsn  13745  fzone1  13832  modsumfzodifsn  14000  seqf1olem1  14097  nprm  16771  4sqlem10  17032  4sqlem17  17046  pgpfaclem2  20185  prmidl0  21515  fvmptnn04ifb  23045  dvferm2lem  26182  lhop2  26211  ftc1lem5  26236  deg1tmle  26312  plyeq0lem  26404  aaliou3lem7  26549  dvloglem  26850  rtprmirr  26962  isosctrlem1  27020  bndatandm  27131  vma1  27367  rplogsumlem2  27686  rpvmasumlem  27688  axlowdimlem13  29341  axlowdimlem16  29344  strlem6  32645  hstrlem6  32653  pmtrto1cl  33450  psgnfzto1stlem  33451  cycpmrn  33494  drngidlhash  33772  krull  33792  esplyfval2  33986  esplyfval3  33993  cos9thpiminply  34209  1smat1  34225  submateqlem1  34228  submateqlem2  34229  xrge0iifcnv  34354  reprlt  35038  reprgt  35040  reprinfz1  35041  erdszelem8  35711  ivthALT  36887  knoppndvlem1  37142  knoppndvlem2  37143  knoppndvlem7  37148  knoppndvlem21  37162  irrdiff  38011  qdiff  38012  poimirlem1  38313  poimirlem6  38318  poimirlem7  38319  poimirlem9  38321  poimirlem15  38327  poimirlem22  38334  3lexlogpow5ineq1  42862  3lexlogpow5ineq2  42863  3lexlogpow5ineq4  42864  3lexlogpow5ineq3  42865  3lexlogpow2ineq1  42866  3lexlogpow2ineq2  42867  3lexlogpow5ineq5  42868  aks4d1lem1  42870  dvrelog2b  42874  0nonelalab  42875  dvrelogpow2b  42876  aks4d1p1p3  42877  aks4d1p1p2  42878  aks4d1p1p4  42879  aks4d1p1p6  42881  aks4d1p1p7  42882  aks4d1p1p5  42883  aks4d1p1  42884  aks4d1p2  42885  aks4d1p3  42886  aks4d1p5  42888  aks4d1p6  42889  aks4d1p7d1  42890  aks4d1p7  42891  aks4d1p8d3  42894  aks4d1p8  42895  aks4d1p9  42896  aks6d1c2p2  42927  aks6d1c3  42931  2np3bcnp1  42952  2ap1caineq  42953  sticksstones1  42954  sticksstones2  42955  sticksstones10  42963  sticksstones12a  42965  sticksstones12  42966  sticksstones22  42976  aks6d1c6lem4  42981  aks6d1c7lem2  42989  aks5lem8  43009  sn-0ne2  43208  radcnvrat  45065  isosctrlem1ALT  45683  ltdiv23neg  46150  lptre2pt  46395  cncfiooicclem1  46648  cncfioobdlem  46651  ditgeqiooicc  46715  itgioocnicc  46732  iblcncfioo  46733  stirlinglem7  46835  fourierdlem34  46896  fourierdlem42  46904  fourierdlem54  46915  fourierdlem60  46921  fourierdlem73  46934  fourierdlem74  46935  fourierdlem76  46937  fourierdlem81  46942  fourierdlem82  46943  fourierdlem84  46945  fourierdlem93  46954  fourierdlem103  46964  fourierdlem104  46965  fourierdlem111  46972  fourierswlem  46985  pimrecltneg  47479  upgrimpthslem2  48714  stgrusgra  48765  eenglngeehlnmlem2  49559