Theorem ltned 11316

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

Syntax hints:   → wi 4   ∈ wcel 2141   ≠ wne 2956   class class class wbr 5099  ℝcr 11069   < clt 11213

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5245  ax-nul 5255  ax-pow 5321  ax-pr 5389  ax-un 7714  ax-resscn 11127  ax-pre-lttri 11144  ax-pre-lttrn 11145

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3745  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-br 5100  df-opab 5162  df-mpt 5181  df-id 5540  df-po 5553  df-so 5554  df-xp 5651  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658  df-iota 6473  df-fun 6519  df-fn 6520  df-f 6521  df-f1 6522  df-fo 6523  df-f1o 6524  df-fv 6525  df-er 8673  df-en 8924  df-dom 8925  df-sdom 8926  df-pnf 11215  df-mnf 11216  df-ltxr 11218

This theorem is referenced by:  fzodisjsn  13700  fzone1  13787  modsumfzodifsn  13954  seqf1olem1  14051  nprm  16705  4sqlem10  16966  4sqlem17  16980  pgpfaclem2  20107  fvmptnn04ifb  22891  dvferm2lem  26028  lhop2  26057  ftc1lem5  26082  deg1tmle  26158  plyeq0lem  26250  aaliou3lem7  26390  dvloglem  26690  rtprmirr  26802  isosctrlem1  26860  bndatandm  26971  vma1  27207  rplogsumlem2  27526  rpvmasumlem  27528  axlowdimlem13  29101  axlowdimlem16  29104  strlem6  32405  hstrlem6  32413  pmtrto1cl  33240  psgnfzto1stlem  33241  cycpmrn  33284  drngidlhash  33581  prmidl0  33598  krull  33628  esplyfval2  33823  esplyfval3  33830  cos9thpiminply  34046  1smat1  34062  submateqlem1  34065  submateqlem2  34066  xrge0iifcnv  34191  reprlt  34877  reprgt  34879  reprinfz1  34880  erdszelem8  35512  ivthALT  36659  knoppndvlem1  36914  knoppndvlem2  36915  knoppndvlem7  36920  knoppndvlem21  36934  irrdiff  37782  qdiff  37783  poimirlem1  38084  poimirlem6  38089  poimirlem7  38090  poimirlem9  38092  poimirlem15  38098  poimirlem22  38105  3lexlogpow5ineq1  42635  3lexlogpow5ineq2  42636  3lexlogpow5ineq4  42637  3lexlogpow5ineq3  42638  3lexlogpow2ineq1  42639  3lexlogpow2ineq2  42640  3lexlogpow5ineq5  42641  aks4d1lem1  42643  dvrelog2b  42647  0nonelalab  42648  dvrelogpow2b  42649  aks4d1p1p3  42650  aks4d1p1p2  42651  aks4d1p1p4  42652  aks4d1p1p6  42654  aks4d1p1p7  42655  aks4d1p1p5  42656  aks4d1p1  42657  aks4d1p2  42658  aks4d1p3  42659  aks4d1p5  42661  aks4d1p6  42662  aks4d1p7d1  42663  aks4d1p7  42664  aks4d1p8d3  42667  aks4d1p8  42668  aks4d1p9  42669  aks6d1c2p2  42700  aks6d1c3  42704  2np3bcnp1  42725  2ap1caineq  42726  sticksstones1  42727  sticksstones2  42728  sticksstones10  42736  sticksstones12a  42738  sticksstones12  42739  sticksstones22  42749  aks6d1c6lem4  42754  aks6d1c7lem2  42762  aks5lem8  42782  sn-0ne2  42979  radcnvrat  44854  isosctrlem1ALT  45473  ltdiv23neg  45933  lptre2pt  46178  cncfiooicclem1  46431  cncfioobdlem  46434  ditgeqiooicc  46498  itgioocnicc  46515  iblcncfioo  46516  stirlinglem7  46618  fourierdlem34  46679  fourierdlem42  46687  fourierdlem54  46698  fourierdlem60  46704  fourierdlem73  46717  fourierdlem74  46718  fourierdlem76  46720  fourierdlem81  46725  fourierdlem82  46726  fourierdlem84  46728  fourierdlem93  46737  fourierdlem103  46747  fourierdlem104  46748  fourierdlem111  46755  fourierswlem  46768  pimrecltneg  47262  upgrimpthslem2  48494  stgrusgra  48545  eenglngeehlnmlem2  49324