Theorem nesymi 3044

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

Syntax hints:  ¬ wn 3   = wceq 1538   ≠ wne 2987

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-ne 2988

This theorem is referenced by:  0nelxp  5553  recgt0ii  11535  xrltnr  12502  nltmnf  12512  xnn0xadd0  12628  fnpr2ob  16823  setcepi  17340  pmtrprfval  18607  pmtrprfvalrn  18608  cnfldfunALT  20104  zringndrg  20183  vieta1lem2  24907  2lgslem3  25988  2lgslem4  25990  structiedg0val  26815  snstriedgval  26831  rusgrnumwwlkl1  27754  clwwlknon1sn  27885  frgrreggt1  28178  1nei  30498  ballotlemi1  31870  sgnnbi  31913  sgnpbi  31914  plymulx0  31927  fmlaomn0  32750  fmla0disjsuc  32758  fmlasucdisj  32759  sltval2  33276  nosgnn0  33278  bj-0nel1  34389  bj-0nelsngl  34407  bj-pr22val  34455  bj-pinftynminfty  34642  finxp0  34808  wepwsolem  39986  refsum2cnlem1  41666  spr0nelg  43993  oddprmALTV  44205