Theorem nesymi 3018

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

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ≠ wne 2961

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758  df-ne 2962

This theorem is used by:  0nelopab  5555  0nelxp  5700  1sdom2dom  9224  recgt0ii  12139  xrltnr  13162  nltmnf  13172  xnn0xadd0  13291  sgnnbi  15167  sgnpbi  15168  fnpr2ob  17637  setcepi  18170  pmtrprfval  19588  pmtrprfvalrn  19589  cnfldfun  21573  zringndrg  21655  plyn0mulidp  26479  vieta1lem2  26509  2lgslem3  27605  2lgslem4  27607  ltsval2  27857  nosgnn0  27859  nogt01o  27897  structiedg0val  29409  snstriedgval  29425  rusgrnumwwlkl1  30357  clwwlknon1sn  30488  frgrreggt1  30781  1nei  33119  rtelextdg2lem  34147  ballotlemi1  34925  fmlaomn0  35903  fmla0disjsuc  35911  fmlasucdisj  35912  bj-0nel1  37630  bj-0nelsngl  37648  bj-pr22val  37696  bj-pinftynminfty  37912  finxp0  38078  wepwsolem  43810  refsum2cnlem1  45798  spr0nelg  48266  oddprmALTV  48493