Theorem nesymi 3012

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1569   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ne 2956

This theorem is used by:  0nelopab  5539  0nelxp  5684  1sdom2dom  9248  recgt0ii  12226  xrltnr  13251  nltmnf  13261  xnn0xadd0  13380  sgnnbi  15262  sgnpbi  15263  fnpr2ob  17735  setcepi  18268  degenmgmnfn  19141  pmtrprfval  19706  pmtrprfvalrn  19707  cnfldfun  21697  zringndrg  21779  plyn0mulidp  26607  vieta1lem2  26639  2lgslem3  27736  2lgslem4  27738  ltsval2  28018  nosgnn0  28020  nogt01o  28058  structiedg0val  29605  snstriedgval  29621  rusgrnumwwlkl1  30565  clwwlknon1sn  30696  frgrreggt1  30999  1nei  33375  rtelextdg2lem  34404  ballotlemi1  35181  fmlaomn0  36241  fmla0disjsuc  36249  fmlasucdisj  36250  bj-0nel1  37958  bj-0nelsngl  37976  bj-pr22val  38024  bj-pinftynminfty  38241  finxp0  38407  wepwsolem  44142  refsum2cnlem1  46147  spr0nelg  48651  oddprmALTV  48878  par2hom  50872