MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nesymi Structured version   Visualization version   GIF version

Theorem nesymi 2998
Description: Inference associated with nesym 2997. (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
StepHypRef Expression
1 nesymi.1 . . 3 𝐴𝐵
21necomi 2995 . 2 𝐵𝐴
32neii 2942 1 ¬ 𝐵 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1541  wne 2940
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ne 2941
This theorem is referenced by:  0nelopab  5566  0nelxp  5709  1sdom2dom  9243  recgt0ii  12116  xrltnr  13095  nltmnf  13105  xnn0xadd0  13222  fnpr2ob  17500  setcepi  18034  pmtrprfval  19349  pmtrprfvalrn  19350  cnfldfun  20948  zringndrg  21029  vieta1lem2  25815  2lgslem3  26896  2lgslem4  26898  sltval2  27148  nosgnn0  27150  nogt01o  27188  structiedg0val  28271  snstriedgval  28287  rusgrnumwwlkl1  29211  clwwlknon1sn  29342  frgrreggt1  29635  1nei  31948  ballotlemi1  33489  sgnnbi  33532  sgnpbi  33533  plymulx0  33546  fmlaomn0  34369  fmla0disjsuc  34377  fmlasucdisj  34378  bj-0nel1  35822  bj-0nelsngl  35840  bj-pr22val  35888  bj-pinftynminfty  36096  finxp0  36260  wepwsolem  41769  refsum2cnlem1  43706  spr0nelg  46130  oddprmALTV  46341
  Copyright terms: Public domain W3C validator