Theorem nesymi 3017

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

Syntax hints:  ¬ wn 3   = wceq 1563   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ne 2961

This theorem is referenced by:  0nelopab  5541  0nelxp  5686  1sdom2dom  9202  recgt0ii  12112  xrltnr  13135  nltmnf  13145  xnn0xadd0  13264  sgnnbi  15131  sgnpbi  15132  fnpr2ob  17602  setcepi  18135  pmtrprfval  19548  pmtrprfvalrn  19549  cnfldfun  21496  zringndrg  21578  plyn0mulidp  26403  vieta1lem2  26433  2lgslem3  27526  2lgslem4  27528  ltsval2  27778  nosgnn0  27780  nogt01o  27818  structiedg0val  29281  snstriedgval  29297  rusgrnumwwlkl1  30229  clwwlknon1sn  30360  frgrreggt1  30653  1nei  32994  rtelextdg2lem  34033  ballotlemi1  34810  fmlaomn0  35753  fmla0disjsuc  35761  fmlasucdisj  35762  bj-0nel1  37450  bj-0nelsngl  37468  bj-pr22val  37516  bj-pinftynminfty  37731  finxp0  37897  wepwsolem  43631  refsum2cnlem1  45615  spr0nelg  48080  oddprmALTV  48307