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

Theorem nesymi 2847
Description: Inference associated with nesym 2846. (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 2844 . 2 𝐵𝐴
32neii 2792 1 ¬ 𝐵 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1480  wne 2790
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-ne 2791
This theorem is referenced by:  0nelxp  5113  recgt0ii  10889  xrltnr  11913  nltmnf  11923  xnn0xadd0  12036  setcepi  16678  pmtrprfval  17847  pmtrprfvalrn  17848  cnfldfunALT  19699  zringndrg  19778  vieta1lem2  24004  2lgslem3  25063  2lgslem4  25065  structiedg0val  25845  snstriedgval  25864  rusgrnumwwlkl1  26764  frgrreggt1  27139  ballotlemi1  30387  sgnnbi  30430  sgnpbi  30431  plymulx0  30446  sltval2  31563  nosgnn0  31565  bj-0nel1  32640  bj-0nelsngl  32659  bj-pr22val  32707  bj-pinftynminfty  32786  finxp0  32899  wepwsolem  37131  refsum2cnlem1  38718  oddprmALTV  40927  spr0nelg  41044
  Copyright terms: Public domain W3C validator