Theorem nesymi 2998

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724  df-ne 2941

This theorem is referenced by:  0nelopab  5567  0nelxp  5710  1sdom2dom  9246  recgt0ii  12119  xrltnr  13098  nltmnf  13108  xnn0xadd0  13225  fnpr2ob  17503  setcepi  18037  pmtrprfval  19354  pmtrprfvalrn  19355  cnfldfun  20955  zringndrg  21037  vieta1lem2  25823  2lgslem3  26904  2lgslem4  26906  sltval2  27156  nosgnn0  27158  nogt01o  27196  structiedg0val  28279  snstriedgval  28295  rusgrnumwwlkl1  29219  clwwlknon1sn  29350  frgrreggt1  29643  1nei  31956  ballotlemi1  33496  sgnnbi  33539  sgnpbi  33540  plymulx0  33553  fmlaomn0  34376  fmla0disjsuc  34384  fmlasucdisj  34385  bj-0nel1  35829  bj-0nelsngl  35847  bj-pr22val  35895  bj-pinftynminfty  36103  finxp0  36267  wepwsolem  41774  refsum2cnlem1  43711  spr0nelg  46134  oddprmALTV  46345