Theorem nesymi 3001

Description: Inference associated with nesym 3000. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)

Hypothesis

Ref	Expression
nesymi.1	⊢ 𝐴 ≠ 𝐵

Assertion

Ref	Expression
nesymi	⊢ ¬ 𝐵 = 𝐴

Proof of Theorem nesymi

Step	Hyp	Ref	Expression
1		nesymi.1	. . 3 ⊢ 𝐴 ≠ 𝐵
2	1	necomi 2998	. 2 ⊢ 𝐵 ≠ 𝐴
3	2	neii 2945	1 ⊢ ¬ 𝐵 = 𝐴

Syntax hints:  ¬ wn 3   = wceq 1539   ≠ wne 2943

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2730  df-ne 2944

This theorem is referenced by:  0nelopab  5480  0nelxp  5623  recgt0ii  11881  xrltnr  12855  nltmnf  12865  xnn0xadd0  12981  fnpr2ob  17269  setcepi  17803  pmtrprfval  19095  pmtrprfvalrn  19096  cnfldfun  20609  zringndrg  20690  vieta1lem2  25471  2lgslem3  26552  2lgslem4  26554  structiedg0val  27392  snstriedgval  27408  rusgrnumwwlkl1  28333  clwwlknon1sn  28464  frgrreggt1  28757  1nei  31071  ballotlemi1  32469  sgnnbi  32512  sgnpbi  32513  plymulx0  32526  fmlaomn0  33352  fmla0disjsuc  33360  fmlasucdisj  33361  sltval2  33859  nosgnn0  33861  nogt01o  33899  bj-0nel1  35143  bj-0nelsngl  35161  bj-pr22val  35209  bj-pinftynminfty  35398  finxp0  35562  wepwsolem  40867  refsum2cnlem1  42580  spr0nelg  44928  oddprmALTV  45139