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

Theorem nesymi 2730
Description: Inference associated with nesym 2729. (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 2727 . 2
32neii 2656 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  =wceq 1395  =/=wne 2652
This theorem is referenced by:  recgt0ii  10476  xrltnr  11359  nltmnf  11367  setcepi  15415  pmtrprfval  16512  pmtrprfvalrn  16513  vieta1lem2  22707  usgraedgprv  24376  2trllemA  24552  2pthon  24604  2pthon3v  24606  4cycl4dv  24667  rusgranumwlkl1  24947  frgrareggt1  25116  ballotlemi1  28441  sgnnbi  28484  sgnpbi  28485  plymulx0  28504  sltval2  29416  nosgnn0  29418  wepwsolem  30987  refsum2cnlem1  31412  bj-0nel1  34509  bj-0nelsngl  34529  bj-pr22val  34577  bj-pinftynminfty  34630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-cleq 2449  df-ne 2654
  Copyright terms: Public domain W3C validator