Theorem nesymi 3014

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ≠ wne 2957

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ne 2958

This theorem is used by:  0nelopab  5548  0nelxp  5693  1sdom2dom  9228  recgt0ii  12149  xrltnr  13174  nltmnf  13184  xnn0xadd0  13303  sgnnbi  15181  sgnpbi  15182  fnpr2ob  17650  setcepi  18183  degenmgmnfn  19055  pmtrprfval  19620  pmtrprfvalrn  19621  cnfldfun  21605  zringndrg  21687  plyn0mulidp  26518  vieta1lem2  26550  2lgslem3  27648  2lgslem4  27650  ltsval2  27900  nosgnn0  27902  nogt01o  27940  structiedg0val  29487  snstriedgval  29503  rusgrnumwwlkl1  30447  clwwlknon1sn  30578  frgrreggt1  30881  1nei  33216  rtelextdg2lem  34244  ballotlemi1  35022  fmlaomn0  35977  fmla0disjsuc  35985  fmlasucdisj  35986  bj-0nel1  37705  bj-0nelsngl  37723  bj-pr22val  37771  bj-pinftynminfty  37987  finxp0  38153  wepwsolem  43891  refsum2cnlem1  45879  spr0nelg  48384  oddprmALTV  48611