Theorem nesymi 2986

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

Syntax hints:  ¬ wn 3   = wceq 1541   ≠ wne 2929

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ne 2930

This theorem is referenced by:  0nelopab  5508  0nelxp  5653  1sdom2dom  9145  recgt0ii  12035  xrltnr  13020  nltmnf  13030  xnn0xadd0  13148  fnpr2ob  17464  setcepi  17997  pmtrprfval  19401  pmtrprfvalrn  19402  cnfldfun  21307  cnfldfunOLD  21320  zringndrg  21407  vieta1lem2  26247  2lgslem3  27343  2lgslem4  27345  sltval2  27596  nosgnn0  27598  nogt01o  27636  structiedg0val  29002  snstriedgval  29018  rusgrnumwwlkl1  29951  clwwlknon1sn  30082  frgrreggt1  30375  1nei  32724  sgnnbi  32826  sgnpbi  32827  rtelextdg2lem  33760  ballotlemi1  34537  plymulx0  34581  fmlaomn0  35455  fmla0disjsuc  35463  fmlasucdisj  35464  bj-0nel1  37018  bj-0nelsngl  37036  bj-pr22val  37084  bj-pinftynminfty  37292  finxp0  37456  wepwsolem  43159  refsum2cnlem1  45158  spr0nelg  47600  oddprmALTV  47811