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

Theorem neii 2945
Description: Inference associated with df-ne 2944. (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 2944 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2mpbi 220 1 ¬ 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1631  wne 2943
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 197  df-ne 2944
This theorem is referenced by:  nesymi  3000  nemtbir  3038  snsssn  4505  2dom  8182  map2xp  8286  updjudhcoinrg  8959  pm54.43lem  9025  canthp1lem2  9677  ine0  10667  inelr  11212  xrltnr  12158  pnfnlt  12167  prprrab  13457  wrdlen2i  13896  3lcm2e6woprm  15536  6lcm4e12  15537  m1dvdsndvds  15710  xpsfrnel2  16433  pmatcollpw3fi1lem1  20811  sinhalfpilem  24436  coseq1  24495  2lgslem3  25350  2lgslem4  25352  axlowdimlem13  26055  axlowdim1  26060  umgredgnlp  26264  wwlksnext  27037  norm1exi  28447  largei  29466  ind1a  30421  ballotlemii  30905  sgnnbi  30947  sgnpbi  30948  dfrdg2  32037  sltval2  32146  nosgnn0  32148  sltintdifex  32151  sltres  32152  sltsolem1  32163  nolt02o  32182  dfrdg4  32395  bj-1nel0  33272  bj-pr21val  33332  finxpreclem2  33564  epnsymrel  34650  0dioph  37868  clsk1indlem1  38869  dirkercncflem2  40838  fourierdlem60  40900  fourierdlem61  40901  fun2dmnopgexmpl  41826
  Copyright terms: Public domain W3C validator