Theorem nesymi 2999

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

Syntax hints:  ¬ wn 3   = wceq 1542   ≠ wne 2941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-ne 2942

This theorem is referenced by:  0nelopab  5568  0nelxp  5711  1sdom2dom  9247  recgt0ii  12120  xrltnr  13099  nltmnf  13109  xnn0xadd0  13226  fnpr2ob  17504  setcepi  18038  pmtrprfval  19355  pmtrprfvalrn  19356  cnfldfun  20956  zringndrg  21038  vieta1lem2  25824  2lgslem3  26907  2lgslem4  26909  sltval2  27159  nosgnn0  27161  nogt01o  27199  structiedg0val  28282  snstriedgval  28298  rusgrnumwwlkl1  29222  clwwlknon1sn  29353  frgrreggt1  29646  1nei  31961  ballotlemi1  33501  sgnnbi  33544  sgnpbi  33545  plymulx0  33558  fmlaomn0  34381  fmla0disjsuc  34389  fmlasucdisj  34390  bj-0nel1  35834  bj-0nelsngl  35852  bj-pr22val  35900  bj-pinftynminfty  36108  finxp0  36272  wepwsolem  41784  refsum2cnlem1  43721  spr0nelg  46144  oddprmALTV  46355