Theorem nesymi 2982

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

Syntax hints:  ¬ wn 3   = wceq 1540   ≠ wne 2925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ne 2926

This theorem is referenced by:  0nelopab  5527  0nelxp  5672  1sdom2dom  9194  recgt0ii  12089  xrltnr  13079  nltmnf  13089  xnn0xadd0  13207  fnpr2ob  17521  setcepi  18050  pmtrprfval  19417  pmtrprfvalrn  19418  cnfldfun  21278  cnfldfunOLD  21291  zringndrg  21378  vieta1lem2  26219  2lgslem3  27315  2lgslem4  27317  sltval2  27568  nosgnn0  27570  nogt01o  27608  structiedg0val  28949  snstriedgval  28965  rusgrnumwwlkl1  29898  clwwlknon1sn  30029  frgrreggt1  30322  1nei  32660  sgnnbi  32763  sgnpbi  32764  rtelextdg2lem  33716  ballotlemi1  34494  plymulx0  34538  fmlaomn0  35377  fmla0disjsuc  35385  fmlasucdisj  35386  bj-0nel1  36941  bj-0nelsngl  36959  bj-pr22val  37007  bj-pinftynminfty  37215  finxp0  37379  wepwsolem  43031  refsum2cnlem1  45031  spr0nelg  47477  oddprmALTV  47688