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

Theorem neii 2653
Description: Inference associated with df-ne 2651. (Contributed by BJ, 7-Jul-2018.)
Hypothesis
Ref Expression
neii.1  |-  A  =/= 
B
Assertion
Ref Expression
neii  |-  -.  A  =  B

Proof of Theorem neii
StepHypRef Expression
1 neii.1 . 2  |-  A  =/= 
B
2 df-ne 2651 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2mpbi 208 1  |-  -.  A  =  B
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1398    =/= wne 2649
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-ne 2651
This theorem is referenced by:  nesymi  2727  nemtbir  2782  snsssn  4184  2dom  7581  map2xp  7680  pm54.43lem  8371  canthp1lem2  9020  ine0  9988  inelr  10521  xrltnr  11333  pnfnlt  11340  wrdlen2i  12875  m1dvdsndvds  14409  xpsfrnel2  15054  pmatcollpw3fi1lem1  19454  sinhalfpilem  23022  coseq1  23081  axlowdimlem13  24459  axlowdim1  24464  usgraedgprv  24578  wlkntrllem3  24765  4cycl4dv  24869  wwlknext  24926  vcoprne  25670  norm1exi  26366  largei  27384  ind1a  28250  ballotlemii  28706  sgnnbi  28748  sgnpbi  28749  dfrdg2  29468  sltval2  29656  nosgnn0  29658  sltintdifex  29663  sltres  29664  sltsolem1  29668  dfrdg4  29828  0dioph  30951  dvnprodlem3  31984  dirkercncflem2  32125  fourierdlem60  32188  fourierdlem61  32189  usgedgnlp  32782  bj-1nel0  34911  bj-pr21val  34972
  Copyright terms: Public domain W3C validator