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

Theorem neii 2642
Description: Inference associated with df-ne 2640. (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 2640 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2mpbi 208 1  |-  -.  A  =  B
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1383    =/= wne 2638
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 2640
This theorem is referenced by:  nesymi  2716  nemtbir  2771  snsssn  4183  2dom  7590  map2xp  7689  pm54.43lem  8383  canthp1lem2  9034  ine0  9998  inelr  10532  xrltnr  11339  pnfnlt  11346  wrdlen2i  12863  m1dvdsndvds  14202  xpsfrnel2  14839  pmatcollpw3fi1lem1  19160  sinhalfpilem  22728  coseq1  22787  axlowdimlem13  24129  axlowdim1  24134  usgraedgprv  24248  wlkntrllem3  24435  4cycl4dv  24539  wwlknext  24596  vcoprne  25344  norm1exi  26040  largei  27058  ind1a  27907  ballotlemii  28315  sgnnbi  28357  sgnpbi  28358  dfrdg2  29203  sltval2  29391  nosgnn0  29393  sltintdifex  29398  sltres  29399  sltsolem1  29403  dfrdg4  29575  0dioph  30687  dirkercncflem2  31775  fourierdlem60  31838  fourierdlem61  31839  usgedgnlp  32248  bj-1nel0  34258  bj-pr21val  34319
  Copyright terms: Public domain W3C validator