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 1541   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

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

This theorem is referenced by:  0nelopab  5513  0nelxp  5658  1sdom2dom  9154  recgt0ii  12048  xrltnr  13033  nltmnf  13043  xnn0xadd0  13162  fnpr2ob  17479  setcepi  18012  pmtrprfval  19416  pmtrprfvalrn  19417  cnfldfun  21323  cnfldfunOLD  21336  zringndrg  21423  vieta1lem2  26275  2lgslem3  27371  2lgslem4  27373  ltsval2  27624  nosgnn0  27626  nogt01o  27664  structiedg0val  29095  snstriedgval  29111  rusgrnumwwlkl1  30044  clwwlknon1sn  30175  frgrreggt1  30468  1nei  32816  sgnnbi  32919  sgnpbi  32920  rtelextdg2lem  33883  ballotlemi1  34660  plymulx0  34704  fmlaomn0  35584  fmla0disjsuc  35592  fmlasucdisj  35593  bj-0nel1  37154  bj-0nelsngl  37172  bj-pr22val  37220  bj-pinftynminfty  37428  finxp0  37592  wepwsolem  43280  refsum2cnlem1  45278  spr0nelg  47718  oddprmALTV  47929