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

Theorem nesymi 2999
Description: Inference associated with nesym 2998. (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 2996 . 2 𝐵𝐴
32neii 2943 1 ¬ 𝐵 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1542  wne 2941
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 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942
This theorem is referenced by:  0nelopab  5568  0nelxp  5711  1sdom2dom  9247  recgt0ii  12120  xrltnr  13099  nltmnf  13109  xnn0xadd0  13226  fnpr2ob  17504  setcepi  18038  pmtrprfval  19355  pmtrprfvalrn  19356  cnfldfun  20956  zringndrg  21038  vieta1lem2  25824  2lgslem3  26907  2lgslem4  26909  sltval2  27159  nosgnn0  27161  nogt01o  27199  structiedg0val  28313  snstriedgval  28329  rusgrnumwwlkl1  29253  clwwlknon1sn  29384  frgrreggt1  29677  1nei  31992  ballotlemi1  33532  sgnnbi  33575  sgnpbi  33576  plymulx0  33589  fmlaomn0  34412  fmla0disjsuc  34420  fmlasucdisj  34421  gg-cnfldfun  35228  bj-0nel1  35882  bj-0nelsngl  35900  bj-pr22val  35948  bj-pinftynminfty  36156  finxp0  36320  wepwsolem  41832  refsum2cnlem1  43769  spr0nelg  46192  oddprmALTV  46403
  Copyright terms: Public domain W3C validator