MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nesymi Structured version   Unicode version

Theorem nesymi 2655
Description: Inference associated with nesym 2654. (Contributed by BJ, 7-Jul-2018.) (Proof shortened by Wolf Lammen, 25-Nov-2019.)
Hypothesis
Ref Expression
nesymi.1  |-  A  =/= 
B
Assertion
Ref Expression
nesymi  |-  -.  B  =  A

Proof of Theorem nesymi
StepHypRef Expression
1 nesymi.1 . . 3  |-  A  =/= 
B
21necomi 2652 . 2  |-  B  =/= 
A
32neii 2581 1  |-  -.  B  =  A
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1399    =/= wne 2577
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-cleq 2374  df-ne 2579
This theorem is referenced by:  recgt0ii  10367  xrltnr  11251  nltmnf  11259  setcepi  15484  pmtrprfval  16629  pmtrprfvalrn  16630  vieta1lem2  22792  usgraedgprv  24497  2trllemA  24673  2pthon  24725  2pthon3v  24727  4cycl4dv  24788  rusgranumwlkl1  25068  frgrareggt1  25237  ballotlemi1  28624  sgnnbi  28667  sgnpbi  28668  plymulx0  28687  sltval2  29581  nosgnn0  29583  wepwsolem  31153  refsum2cnlem1  31579  oddprmALTV  32529  bj-0nel1  34857  bj-0nelsngl  34877  bj-pr22val  34925  bj-pinftynminfty  34977
  Copyright terms: Public domain W3C validator