Theorem nesymi 2997

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

Syntax hints:  ¬ wn 3   = wceq 1539   ≠ wne 2939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2728  df-ne 2940

This theorem is referenced by:  0nelopab  5571  0nelxp  5718  1sdom2dom  9284  recgt0ii  12175  xrltnr  13162  nltmnf  13172  xnn0xadd0  13290  fnpr2ob  17604  setcepi  18134  pmtrprfval  19506  pmtrprfvalrn  19507  cnfldfun  21379  cnfldfunOLD  21392  zringndrg  21480  vieta1lem2  26354  2lgslem3  27449  2lgslem4  27451  sltval2  27702  nosgnn0  27704  nogt01o  27742  structiedg0val  29040  snstriedgval  29056  rusgrnumwwlkl1  29989  clwwlknon1sn  30120  frgrreggt1  30413  1nei  32748  rtelextdg2lem  33768  ballotlemi1  34506  sgnnbi  34549  sgnpbi  34550  plymulx0  34563  fmlaomn0  35396  fmla0disjsuc  35404  fmlasucdisj  35405  bj-0nel1  36955  bj-0nelsngl  36973  bj-pr22val  37021  bj-pinftynminfty  37229  finxp0  37393  wepwsolem  43059  refsum2cnlem1  45047  spr0nelg  47468  oddprmALTV  47679