Theorem nesymi 2989

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

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

This theorem is referenced by:  0nelopab  5520  0nelxp  5665  1sdom2dom  9164  recgt0ii  12062  xrltnr  13070  nltmnf  13080  xnn0xadd0  13199  fnpr2ob  17522  setcepi  18055  pmtrprfval  19462  pmtrprfvalrn  19463  cnfldfun  21366  zringndrg  21448  vieta1lem2  26277  2lgslem3  27367  2lgslem4  27369  ltsval2  27620  nosgnn0  27622  nogt01o  27660  structiedg0val  29091  snstriedgval  29107  rusgrnumwwlkl1  30039  clwwlknon1sn  30170  frgrreggt1  30463  1nei  32810  sgnnbi  32911  sgnpbi  32912  rtelextdg2lem  33870  ballotlemi1  34647  plymulx0  34691  fmlaomn0  35572  fmla0disjsuc  35580  fmlasucdisj  35581  bj-0nel1  37260  bj-0nelsngl  37278  bj-pr22val  37326  bj-pinftynminfty  37541  finxp0  37707  wepwsolem  43470  refsum2cnlem1  45468  spr0nelg  47936  oddprmALTV  48163