Theorem nesymi 2992

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

Syntax hints:  ¬ wn 3   = wceq 1547   ≠ wne 2935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ne 2936

This theorem is referenced by:  0nelopab  5514  0nelxp  5659  1sdom2dom  9161  recgt0ii  12060  xrltnr  13068  nltmnf  13078  xnn0xadd0  13197  fnpr2ob  17520  setcepi  18053  pmtrprfval  19460  pmtrprfvalrn  19461  cnfldfun  21368  zringndrg  21450  vieta1lem2  26302  2lgslem3  27392  2lgslem4  27394  ltsval2  27645  nosgnn0  27647  nogt01o  27685  structiedg0val  29116  snstriedgval  29132  rusgrnumwwlkl1  30064  clwwlknon1sn  30195  frgrreggt1  30488  1nei  32836  sgnnbi  32937  sgnpbi  32938  rtelextdg2lem  33917  ballotlemi1  34694  plymulx0  34738  fmlaomn0  35625  fmla0disjsuc  35633  fmlasucdisj  35634  bj-0nel1  37313  bj-0nelsngl  37331  bj-pr22val  37379  bj-pinftynminfty  37594  finxp0  37760  wepwsolem  43494  refsum2cnlem1  45492  spr0nelg  47958  oddprmALTV  48185