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

Theorem nesymi 3070
Description: Inference associated with nesym 3069. (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 3067 . 2 𝐵𝐴
32neii 3015 1 ¬ 𝐵 = 𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1528  wne 3013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-ne 3014
This theorem is referenced by:  0nelxp  5582  recgt0ii  11534  xrltnr  12502  nltmnf  12512  xnn0xadd0  12628  fnpr2ob  16819  setcepi  17336  pmtrprfval  18544  pmtrprfvalrn  18545  cnfldfunALT  20486  zringndrg  20565  vieta1lem2  24827  2lgslem3  25907  2lgslem4  25909  structiedg0val  26734  snstriedgval  26750  rusgrnumwwlkl1  27674  clwwlknon1sn  27806  frgrreggt1  28099  1nei  30398  ballotlemi1  31659  sgnnbi  31702  sgnpbi  31703  plymulx0  31716  fmlaomn0  32534  fmla0disjsuc  32542  fmlasucdisj  32543  sltval2  33060  nosgnn0  33062  bj-0nel1  34162  bj-0nelsngl  34180  bj-pr22val  34228  bj-pinftynminfty  34401  finxp0  34554  wepwsolem  39520  refsum2cnlem1  41171  spr0nelg  43515  oddprmALTV  43729
  Copyright terms: Public domain W3C validator