Theorem nesymi 3000

Description: Inference associated with nesym 2999. (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 2997	. 2 ⊢ 𝐵 ≠ 𝐴
3	2	neii 2944	1 ⊢ ¬ 𝐵 = 𝐴

Syntax hints:  ¬ wn 3   = wceq 1539   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730  df-ne 2943

This theorem is referenced by:  0nelopab  5471  0nelxp  5614  recgt0ii  11811  xrltnr  12784  nltmnf  12794  xnn0xadd0  12910  fnpr2ob  17186  setcepi  17719  pmtrprfval  19010  pmtrprfvalrn  19011  cnfldfunALT  20523  zringndrg  20602  vieta1lem2  25376  2lgslem3  26457  2lgslem4  26459  structiedg0val  27295  snstriedgval  27311  rusgrnumwwlkl1  28234  clwwlknon1sn  28365  frgrreggt1  28658  1nei  30973  ballotlemi1  32369  sgnnbi  32412  sgnpbi  32413  plymulx0  32426  fmlaomn0  33252  fmla0disjsuc  33260  fmlasucdisj  33261  sltval2  33786  nosgnn0  33788  nogt01o  33826  bj-0nel1  35070  bj-0nelsngl  35088  bj-pr22val  35136  bj-pinftynminfty  35325  finxp0  35489  wepwsolem  40783  refsum2cnlem1  42469  spr0nelg  44816  oddprmALTV  45027