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  5513  0nelxp  5658  1sdom2dom  9157  recgt0ii  12053  xrltnr  13061  nltmnf  13071  xnn0xadd0  13190  fnpr2ob  17513  setcepi  18046  pmtrprfval  19453  pmtrprfvalrn  19454  cnfldfun  21358  cnfldfunOLD  21371  zringndrg  21458  vieta1lem2  26288  2lgslem3  27381  2lgslem4  27383  ltsval2  27634  nosgnn0  27636  nogt01o  27674  structiedg0val  29105  snstriedgval  29121  rusgrnumwwlkl1  30054  clwwlknon1sn  30185  frgrreggt1  30478  1nei  32825  sgnnbi  32926  sgnpbi  32927  rtelextdg2lem  33886  ballotlemi1  34663  plymulx0  34707  fmlaomn0  35588  fmla0disjsuc  35596  fmlasucdisj  35597  bj-0nel1  37276  bj-0nelsngl  37294  bj-pr22val  37342  bj-pinftynminfty  37557  finxp0  37721  wepwsolem  43488  refsum2cnlem1  45486  spr0nelg  47948  oddprmALTV  48175