Theorem nesymi 2851

Description: Inference associated with nesym 2850. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)

Hypothesis

Ref	Expression
nesymi.1	|- A =/= B

Assertion

Ref	Expression
nesymi	|- -. B = A

Proof of Theorem nesymi

Step	Hyp	Ref	Expression
1		nesymi.1	. . 3 |- A =/= B
2	1	necomi 2848	. 2 |- B =/= A
3	2	neii 2796	1 |- -. B = A

Syntax hints:   -. wn 3   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-ne 2795

This theorem is referenced by:  0nelxp  5143  recgt0ii  10929  xrltnr  11953  nltmnf  11963  xnn0xadd0  12077  setcepi  16738  pmtrprfval  17907  pmtrprfvalrn  17908  cnfldfunALT  19759  zringndrg  19838  vieta1lem2  24066  2lgslem3  25129  2lgslem4  25131  structiedg0val  25911  snstriedgval  25930  rusgrnumwwlkl1  26863  frgrreggt1  27251  ballotlemi1  30564  sgnnbi  30607  sgnpbi  30608  plymulx0  30624  sltval2  31809  nosgnn0  31811  bj-0nel1  32940  bj-0nelsngl  32959  bj-pr22val  33007  bj-pinftynminfty  33114  finxp0  33228  wepwsolem  37612  refsum2cnlem1  39196  oddprmALTV  41598  spr0nelg  41726