Theorem nesymi 3015

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

Syntax hints:  ¬ wn 3   = wceq 1570   ≠ wne 2958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ne 2959

This theorem is referenced by:  0nelopab  5552  0nelxp  5697  1sdom2dom  9215  recgt0ii  12122  xrltnr  13145  nltmnf  13155  xnn0xadd0  13274  sgnnbi  15143  sgnpbi  15144  fnpr2ob  17613  setcepi  18146  pmtrprfval  19558  pmtrprfvalrn  19559  cnfldfun  21517  zringndrg  21599  plyn0mulidp  26423  vieta1lem2  26453  2lgslem3  27546  2lgslem4  27548  ltsval2  27798  nosgnn0  27800  nogt01o  27838  structiedg0val  29350  snstriedgval  29366  rusgrnumwwlkl1  30298  clwwlknon1sn  30429  frgrreggt1  30722  1nei  33060  rtelextdg2lem  34094  ballotlemi1  34871  fmlaomn0  35860  fmla0disjsuc  35868  fmlasucdisj  35869  bj-0nel1  37567  bj-0nelsngl  37585  bj-pr22val  37633  bj-pinftynminfty  37849  finxp0  38015  wepwsolem  43749  refsum2cnlem1  45737  spr0nelg  48202  oddprmALTV  48429