Theorem nesymi 3032

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

Syntax hints:  ¬ wn 3   = wceq 1653   ≠ wne 2975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-ext 2781

This theorem depends on definitions:  df-bi 199  df-an 386  df-ex 1876  df-cleq 2796  df-ne 2976

This theorem is referenced by:  0nelxp  5350  recgt0ii  11225  xrltnr  12204  nltmnf  12214  xnn0xadd0  12330  setcepi  17056  pmtrprfval  18223  pmtrprfvalrn  18224  cnfldfunALT  20085  zringndrg  20164  vieta1lem2  24411  2lgslem3  25485  2lgslem4  25487  structiedg0val  26261  snstriedgval  26277  rusgrnumwwlkl1  27263  clwwlknon1sn  27443  frgrreggt1  27782  ballotlemi1  31085  sgnnbi  31128  sgnpbi  31129  plymulx0  31146  sltval2  32326  nosgnn0  32328  bj-0nel1  33436  bj-0nelsngl  33455  bj-pr22val  33503  bj-pinftynminfty  33617  finxp0  33730  wepwsolem  38401  refsum2cnlem1  39960  oddprmALTV  42384  spr0nelg  42529