Theorem nesymi 2983

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

Syntax hints:  ¬ wn 3   = wceq 1540   ≠ wne 2926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ne 2927

This theorem is referenced by:  0nelopab  5530  0nelxp  5675  1sdom2dom  9201  recgt0ii  12096  xrltnr  13086  nltmnf  13096  xnn0xadd0  13214  fnpr2ob  17528  setcepi  18057  pmtrprfval  19424  pmtrprfvalrn  19425  cnfldfun  21285  cnfldfunOLD  21298  zringndrg  21385  vieta1lem2  26226  2lgslem3  27322  2lgslem4  27324  sltval2  27575  nosgnn0  27577  nogt01o  27615  structiedg0val  28956  snstriedgval  28972  rusgrnumwwlkl1  29905  clwwlknon1sn  30036  frgrreggt1  30329  1nei  32667  sgnnbi  32770  sgnpbi  32771  rtelextdg2lem  33723  ballotlemi1  34501  plymulx0  34545  fmlaomn0  35384  fmla0disjsuc  35392  fmlasucdisj  35393  bj-0nel1  36948  bj-0nelsngl  36966  bj-pr22val  37014  bj-pinftynminfty  37222  finxp0  37386  wepwsolem  43038  refsum2cnlem1  45038  spr0nelg  47481  oddprmALTV  47692