Theorem nesymi 3004

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ne 2947

This theorem is referenced by:  0nelopab  5586  0nelxp  5734  1sdom2dom  9310  recgt0ii  12201  xrltnr  13182  nltmnf  13192  xnn0xadd0  13309  fnpr2ob  17618  setcepi  18155  pmtrprfval  19529  pmtrprfvalrn  19530  cnfldfun  21401  cnfldfunOLD  21414  zringndrg  21502  vieta1lem2  26371  2lgslem3  27466  2lgslem4  27468  sltval2  27719  nosgnn0  27721  nogt01o  27759  structiedg0val  29057  snstriedgval  29073  rusgrnumwwlkl1  30001  clwwlknon1sn  30132  frgrreggt1  30425  1nei  32750  rtelextdg2lem  33717  ballotlemi1  34467  sgnnbi  34510  sgnpbi  34511  plymulx0  34524  fmlaomn0  35358  fmla0disjsuc  35366  fmlasucdisj  35367  bj-0nel1  36919  bj-0nelsngl  36937  bj-pr22val  36985  bj-pinftynminfty  37193  finxp0  37357  wepwsolem  42999  refsum2cnlem1  44937  spr0nelg  47350  oddprmALTV  47561