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

Theorem nesymi 2721
Description: Inference associated with nesym 2720. (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 2718 . 2  |-  B  =/= 
A
32neii 2648 1  |-  -.  B  =  A
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1370    =/= wne 2644
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-cleq 2443  df-ne 2646
This theorem is referenced by:  recgt0ii  10341  xrltnr  11204  nltmnf  11212  setcepi  15060  pmtrprfval  16097  pmtrprfvalrn  16098  vieta1lem2  21895  usgraedgprv  23432  2trllemA  23586  2pthon  23638  2pthon3v  23640  4cycl4dv  23690  sgnpbi  27065  plymulx0  27084  rusgranumwlkl1  30699  frgrareggt1  30849  bj-0nel1  32746  bj-0nelsngl  32766  bj-pr22val  32814  bj-pinftynminfty  32858
  Copyright terms: Public domain W3C validator