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

Step	Hyp	Ref	Expression
1		nesymi.1	. . 3
2	1	necomi 2727	. 2
3	2	neii 2656	1

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