Theorem nesymi 2985

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

Syntax hints:  ¬ wn 3   = wceq 1541   ≠ wne 2928

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ne 2929

This theorem is referenced by:  0nelopab  5505  0nelxp  5650  1sdom2dom  9138  recgt0ii  12025  xrltnr  13015  nltmnf  13025  xnn0xadd0  13143  fnpr2ob  17459  setcepi  17992  pmtrprfval  19397  pmtrprfvalrn  19398  cnfldfun  21303  cnfldfunOLD  21316  zringndrg  21403  vieta1lem2  26244  2lgslem3  27340  2lgslem4  27342  sltval2  27593  nosgnn0  27595  nogt01o  27633  structiedg0val  28998  snstriedgval  29014  rusgrnumwwlkl1  29944  clwwlknon1sn  30075  frgrreggt1  30368  1nei  32715  sgnnbi  32816  sgnpbi  32817  rtelextdg2lem  33734  ballotlemi1  34511  plymulx0  34555  fmlaomn0  35422  fmla0disjsuc  35430  fmlasucdisj  35431  bj-0nel1  36986  bj-0nelsngl  37004  bj-pr22val  37052  bj-pinftynminfty  37260  finxp0  37424  wepwsolem  43074  refsum2cnlem1  45073  spr0nelg  47506  oddprmALTV  47717