Theorem nesymi 2990

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

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

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 2708

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

This theorem is referenced by:  0nelopab  5547  0nelxp  5693  1sdom2dom  9260  recgt0ii  12153  xrltnr  13140  nltmnf  13150  xnn0xadd0  13268  fnpr2ob  17577  setcepi  18106  pmtrprfval  19473  pmtrprfvalrn  19474  cnfldfun  21334  cnfldfunOLD  21347  zringndrg  21434  vieta1lem2  26276  2lgslem3  27372  2lgslem4  27374  sltval2  27625  nosgnn0  27627  nogt01o  27665  structiedg0val  29006  snstriedgval  29022  rusgrnumwwlkl1  29955  clwwlknon1sn  30086  frgrreggt1  30379  1nei  32719  sgnnbi  32822  sgnpbi  32823  rtelextdg2lem  33765  ballotlemi1  34540  plymulx0  34584  fmlaomn0  35417  fmla0disjsuc  35425  fmlasucdisj  35426  bj-0nel1  36976  bj-0nelsngl  36994  bj-pr22val  37042  bj-pinftynminfty  37250  finxp0  37414  wepwsolem  43033  refsum2cnlem1  45028  spr0nelg  47457  oddprmALTV  47668