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

Theorem neii 2656
Description: Inference associated with df-ne 2654. (Contributed by BJ, 7-Jul-2018.)
Hypothesis
Ref Expression
neii.1
Assertion
Ref Expression
neii

Proof of Theorem neii
StepHypRef Expression
1 neii.1 . 2
2 df-ne 2654 . 2
31, 2mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  =wceq 1395  =/=wne 2652
This theorem is referenced by:  nesymi  2730  nemtbir  2785  snsssn  4198  2dom  7608  map2xp  7707  pm54.43lem  8401  canthp1lem2  9052  ine0  10017  inelr  10551  xrltnr  11359  pnfnlt  11366  wrdlen2i  12884  m1dvdsndvds  14325  xpsfrnel2  14962  pmatcollpw3fi1lem1  19287  sinhalfpilem  22856  coseq1  22915  axlowdimlem13  24257  axlowdim1  24262  usgraedgprv  24376  wlkntrllem3  24563  4cycl4dv  24667  wwlknext  24724  vcoprne  25472  norm1exi  26168  largei  27186  ind1a  28034  ballotlemii  28442  sgnnbi  28484  sgnpbi  28485  dfrdg2  29228  sltval2  29416  nosgnn0  29418  sltintdifex  29423  sltres  29424  sltsolem1  29428  dfrdg4  29600  0dioph  30712  dvnprodlem3  31745  dirkercncflem2  31886  fourierdlem60  31949  fourierdlem61  31950  usgedgnlp  32410  bj-1nel0  34510  bj-pr21val  34571
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 2654
  Copyright terms: Public domain W3C validator