Theorem nesymi 2989

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

Syntax hints:  ¬ wn 3   = wceq 1632   ≠ wne 2932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-ne 2933

This theorem is referenced by:  0nelxp  5300  recgt0ii  11121  xrltnr  12146  nltmnf  12156  xnn0xadd0  12270  setcepi  16939  pmtrprfval  18107  pmtrprfvalrn  18108  cnfldfunALT  19961  zringndrg  20040  vieta1lem2  24265  2lgslem3  25328  2lgslem4  25330  structiedg0val  26110  snstriedgval  26129  rusgrnumwwlkl1  27090  clwwlknon1sn  27248  frgrreggt1  27561  ballotlemi1  30873  sgnnbi  30916  sgnpbi  30917  plymulx0  30933  sltval2  32115  nosgnn0  32117  bj-0nel1  33246  bj-0nelsngl  33265  bj-pr22val  33313  bj-pinftynminfty  33425  finxp0  33539  wepwsolem  38114  refsum2cnlem1  39695  oddprmALTV  42108  spr0nelg  42236