Theorem nesymi 3013

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

Syntax hints:  ¬ wn 3   = wceq 1559   ≠ wne 2956

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ne 2957

This theorem is referenced by:  0nelopab  5534  0nelxp  5679  1sdom2dom  9194  recgt0ii  12095  xrltnr  13118  nltmnf  13128  xnn0xadd0  13247  fnpr2ob  17571  setcepi  18104  pmtrprfval  19510  pmtrprfvalrn  19511  cnfldfun  21418  zringndrg  21500  vieta1lem2  26352  2lgslem3  27445  2lgslem4  27447  ltsval2  27697  nosgnn0  27699  nogt01o  27737  structiedg0val  29169  snstriedgval  29185  rusgrnumwwlkl1  30117  clwwlknon1sn  30248  frgrreggt1  30541  1nei  32889  sgnnbi  32990  sgnpbi  32991  rtelextdg2lem  33984  ballotlemi1  34761  plymulx0  34805  fmlaomn0  35704  fmla0disjsuc  35712  fmlasucdisj  35713  bj-0nel1  37402  bj-0nelsngl  37420  bj-pr22val  37468  bj-pinftynminfty  37683  finxp0  37849  wepwsolem  43583  refsum2cnlem1  45581  spr0nelg  48046  oddprmALTV  48273