Theorem nesymi 3075

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

Syntax hints:  ¬ wn 3   = wceq 1537   ≠ wne 3018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2816  df-ne 3019

This theorem is referenced by:  0nelxp  5591  recgt0ii  11548  xrltnr  12517  nltmnf  12527  xnn0xadd0  12643  fnpr2ob  16833  setcepi  17350  pmtrprfval  18617  pmtrprfvalrn  18618  cnfldfunALT  20560  zringndrg  20639  vieta1lem2  24902  2lgslem3  25982  2lgslem4  25984  structiedg0val  26809  snstriedgval  26825  rusgrnumwwlkl1  27749  clwwlknon1sn  27881  frgrreggt1  28174  1nei  30474  ballotlemi1  31762  sgnnbi  31805  sgnpbi  31806  plymulx0  31819  fmlaomn0  32639  fmla0disjsuc  32647  fmlasucdisj  32648  sltval2  33165  nosgnn0  33167  bj-0nel1  34267  bj-0nelsngl  34285  bj-pr22val  34333  bj-pinftynminfty  34511  finxp0  34674  wepwsolem  39649  refsum2cnlem1  41301  spr0nelg  43645  oddprmALTV  43859