Theorem nesymi 3016

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ≠ wne 2959

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ne 2960

This theorem is used by:  0nelopab  5544  0nelxp  5689  1sdom2dom  9273  recgt0ii  12250  xrltnr  13275  nltmnf  13285  xnn0xadd0  13404  sgnnbi  15286  sgnpbi  15287  fnpr2ob  17759  setcepi  18292  degenmgmnfn  19165  pmtrprfval  19731  pmtrprfvalrn  19732  cnfldfun  21722  zringndrg  21804  plyn0mulidp  26632  vieta1lem2  26664  2lgslem3  27761  2lgslem4  27763  ltsval2  28043  nosgnn0  28045  nogt01o  28083  structiedg0val  29630  snstriedgval  29646  rusgrnumwwlkl1  30590  clwwlknon1sn  30721  frgrreggt1  31024  1nei  33399  rtelextdg2lem  34428  ballotlemi1  35205  fmlaomn0  36322  fmla0disjsuc  36330  fmlasucdisj  36331  bj-0nel1  38044  bj-0nelsngl  38062  bj-pr22val  38110  bj-pinftynminfty  38340  finxp0  38506  wepwsolem  44242  refsum2cnlem1  46259  spr0nelg  48763  oddprmALTV  48990  par2hom  50984