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

Theorem nesymi 2989
 Description: Inference associated with nesym 2988. (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 2986 . 2 𝐵𝐴
32neii 2934 1 ¬ 𝐵 = 𝐴
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1632   ≠ wne 2932 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740 This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-ne 2933 This theorem is referenced by:  0nelxp  5300  recgt0ii  11121  xrltnr  12146  nltmnf  12156  xnn0xadd0  12270  setcepi  16939  pmtrprfval  18107  pmtrprfvalrn  18108  cnfldfunALT  19961  zringndrg  20040  vieta1lem2  24265  2lgslem3  25328  2lgslem4  25330  structiedg0val  26110  snstriedgval  26129  rusgrnumwwlkl1  27090  clwwlknon1sn  27248  frgrreggt1  27561  ballotlemi1  30873  sgnnbi  30916  sgnpbi  30917  plymulx0  30933  sltval2  32115  nosgnn0  32117  bj-0nel1  33246  bj-0nelsngl  33265  bj-pr22val  33313  bj-pinftynminfty  33425  finxp0  33539  wepwsolem  38114  refsum2cnlem1  39695  oddprmALTV  42108  spr0nelg  42236
 Copyright terms: Public domain W3C validator