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

Theorem nesymi 3002
Description: Inference associated with nesym 3001. (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 2999 . 2 𝐵𝐴
32neii 2946 1 ¬ 𝐵 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1542  wne 2944
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2729  df-ne 2945
This theorem is referenced by:  0nelopab  5529  0nelxp  5672  1sdom2dom  9198  recgt0ii  12068  xrltnr  13047  nltmnf  13057  xnn0xadd0  13173  fnpr2ob  17447  setcepi  17981  pmtrprfval  19276  pmtrprfvalrn  19277  cnfldfun  20824  zringndrg  20905  vieta1lem2  25687  2lgslem3  26768  2lgslem4  26770  sltval2  27020  nosgnn0  27022  nogt01o  27060  structiedg0val  28015  snstriedgval  28031  rusgrnumwwlkl1  28955  clwwlknon1sn  29086  frgrreggt1  29379  1nei  31695  ballotlemi1  33142  sgnnbi  33185  sgnpbi  33186  plymulx0  33199  fmlaomn0  34024  fmla0disjsuc  34032  fmlasucdisj  34033  bj-0nel1  35453  bj-0nelsngl  35471  bj-pr22val  35519  bj-pinftynminfty  35727  finxp0  35891  wepwsolem  41398  refsum2cnlem1  43316  spr0nelg  45742  oddprmALTV  45953
  Copyright terms: Public domain W3C validator