Theorem nesymi 3013

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

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

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 2733

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

This theorem is used by:  0nelopab  5540  0nelxp  5685  1sdom2dom  9229  recgt0ii  12204  xrltnr  13229  nltmnf  13239  xnn0xadd0  13358  sgnnbi  15237  sgnpbi  15238  fnpr2ob  17710  setcepi  18243  degenmgmnfn  19116  pmtrprfval  19681  pmtrprfvalrn  19682  cnfldfun  21672  zringndrg  21754  plyn0mulidp  26584  vieta1lem2  26616  2lgslem3  27713  2lgslem4  27715  ltsval2  27995  nosgnn0  27997  nogt01o  28035  structiedg0val  29582  snstriedgval  29598  rusgrnumwwlkl1  30542  clwwlknon1sn  30673  frgrreggt1  30976  1nei  33311  rtelextdg2lem  34340  ballotlemi1  35118  fmlaomn0  36124  fmla0disjsuc  36132  fmlasucdisj  36133  bj-0nel1  37836  bj-0nelsngl  37854  bj-pr22val  37902  bj-pinftynminfty  38116  finxp0  38282  wepwsolem  44002  refsum2cnlem1  45997  spr0nelg  48502  oddprmALTV  48729