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

Theorem nesymi 3032
Description: Inference associated with nesym 3031. (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 3029 . 2 𝐵𝐴
32neii 2977 1 ¬ 𝐵 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1653  wne 2975
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2781
This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2796  df-ne 2976
This theorem is referenced by:  0nelxp  5350  recgt0ii  11225  xrltnr  12204  nltmnf  12214  xnn0xadd0  12330  setcepi  17056  pmtrprfval  18223  pmtrprfvalrn  18224  cnfldfunALT  20085  zringndrg  20164  vieta1lem2  24411  2lgslem3  25485  2lgslem4  25487  structiedg0val  26261  snstriedgval  26277  rusgrnumwwlkl1  27263  clwwlknon1sn  27443  frgrreggt1  27782  ballotlemi1  31085  sgnnbi  31128  sgnpbi  31129  plymulx0  31146  sltval2  32326  nosgnn0  32328  bj-0nel1  33436  bj-0nelsngl  33455  bj-pr22val  33503  bj-pinftynminfty  33617  finxp0  33730  wepwsolem  38401  refsum2cnlem1  39960  oddprmALTV  42384  spr0nelg  42529
  Copyright terms: Public domain W3C validator