Theorem nesymi 2990

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

Syntax hints:  ¬ wn 3   = wceq 1542   ≠ wne 2933

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ne 2934

This theorem is referenced by:  0nelopab  5521  0nelxp  5666  1sdom2dom  9166  recgt0ii  12060  xrltnr  13045  nltmnf  13055  xnn0xadd0  13174  fnpr2ob  17491  setcepi  18024  pmtrprfval  19428  pmtrprfvalrn  19429  cnfldfun  21335  cnfldfunOLD  21348  zringndrg  21435  vieta1lem2  26287  2lgslem3  27383  2lgslem4  27385  ltsval2  27636  nosgnn0  27638  nogt01o  27676  structiedg0val  29107  snstriedgval  29123  rusgrnumwwlkl1  30056  clwwlknon1sn  30187  frgrreggt1  30480  1nei  32826  sgnnbi  32929  sgnpbi  32930  rtelextdg2lem  33903  ballotlemi1  34680  plymulx0  34724  fmlaomn0  35603  fmla0disjsuc  35611  fmlasucdisj  35612  bj-0nel1  37195  bj-0nelsngl  37213  bj-pr22val  37261  bj-pinftynminfty  37476  finxp0  37640  wepwsolem  43393  refsum2cnlem1  45391  spr0nelg  47830  oddprmALTV  48041