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

Theorem nesymi 3073
Description: Inference associated with nesym 3072. (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 3070 . 2 𝐵𝐴
32neii 3018 1 ¬ 𝐵 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1533  wne 3016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-ne 3017
This theorem is referenced by:  0nelxp  5583  recgt0ii  11540  xrltnr  12508  nltmnf  12518  xnn0xadd0  12634  fnpr2ob  16825  setcepi  17342  pmtrprfval  18609  pmtrprfvalrn  18610  cnfldfunALT  20552  zringndrg  20631  vieta1lem2  24894  2lgslem3  25974  2lgslem4  25976  structiedg0val  26801  snstriedgval  26817  rusgrnumwwlkl1  27741  clwwlknon1sn  27873  frgrreggt1  28166  1nei  30466  ballotlemi1  31755  sgnnbi  31798  sgnpbi  31799  plymulx0  31812  fmlaomn0  32632  fmla0disjsuc  32640  fmlasucdisj  32641  sltval2  33158  nosgnn0  33160  bj-0nel1  34260  bj-0nelsngl  34278  bj-pr22val  34326  bj-pinftynminfty  34503  finxp0  34666  wepwsolem  39635  refsum2cnlem1  41287  spr0nelg  43632  oddprmALTV  43846
  Copyright terms: Public domain W3C validator