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

Theorem nesymi 2835
Description: Inference associated with nesym 2834. (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 2832 . 2 𝐵𝐴
32neii 2780 1 ¬ 𝐵 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1474  wne 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-cleq 2599  df-ne 2778
This theorem is referenced by:  0nelxp  5054  recgt0ii  10775  xrltnr  11787  nltmnf  11797  setcepi  16504  pmtrprfval  17673  pmtrprfvalrn  17674  vieta1lem2  23784  2lgslem3  24843  2lgslem4  24845  usgraedgprv  25668  2trllemA  25843  2pthon  25895  2pthon3v  25897  4cycl4dv  25958  rusgranumwlkl1  26237  frgrareggt1  26406  ballotlemi1  29694  sgnnbi  29737  sgnpbi  29738  plymulx0  29753  sltval2  30856  nosgnn0  30858  bj-0nel1  31933  bj-0nelsngl  31952  bj-pr22val  32000  bj-pinftynminfty  32091  finxp0  32204  wepwsolem  36430  refsum2cnlem1  38019  oddprmALTV  39938  xnn0xadd0  40214  structiedg0val  40254  snstriedgval  40268  rusgrnumwwlkl1  41171  av-frgrareggt1  41546
  Copyright terms: Public domain W3C validator