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  5512  0nelxp  5657  1sdom2dom  9153  recgt0ii  12049  xrltnr  13039  nltmnf  13049  xnn0xadd0  13167  fnpr2ob  17480  setcepi  18013  pmtrprfval  19384  pmtrprfvalrn  19385  cnfldfun  21293  cnfldfunOLD  21306  zringndrg  21393  vieta1lem2  26235  2lgslem3  27331  2lgslem4  27333  sltval2  27584  nosgnn0  27586  nogt01o  27624  structiedg0val  28985  snstriedgval  29001  rusgrnumwwlkl1  29931  clwwlknon1sn  30062  frgrreggt1  30355  1nei  32693  sgnnbi  32796  sgnpbi  32797  rtelextdg2lem  33692  ballotlemi1  34470  plymulx0  34514  fmlaomn0  35362  fmla0disjsuc  35370  fmlasucdisj  35371  bj-0nel1  36926  bj-0nelsngl  36944  bj-pr22val  36992  bj-pinftynminfty  37200  finxp0  37364  wepwsolem  43015  refsum2cnlem1  45015  spr0nelg  47461  oddprmALTV  47672