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

Theorem neii 3009
Description: Inference associated with df-ne 3008. (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 3008 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2mpbi 233 1 ¬ 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1538  wne 3007
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 210  df-ne 3008
This theorem is referenced by:  nesymi  3064  nemtbir  3102  snsssn  4745  2dom  8557  map2xp  8663  updjudhcoinrg  9338  pm54.43lem  9405  canthp1lem2  10052  ine0  11052  inelr  11605  xrltnr  12492  pnfnlt  12501  prprrab  13815  wrdlen2i  14283  3lcm2e6woprm  15936  6lcm4e12  15937  m1dvdsndvds  16112  fnpr2ob  16809  fvprif  16812  pmatcollpw3fi1lem1  21369  sinhalfpilem  25034  coseq1  25095  2lgslem3  25966  2lgslem4  25968  axlowdimlem13  26726  axlowdim1  26731  umgredgnlp  26918  wwlksnext  27657  norm1exi  29011  largei  30028  ind1a  31285  ballotlemii  31768  sgnnbi  31810  sgnpbi  31811  gonanegoal  32606  gonan0  32646  goaln0  32647  fmlasucdisj  32653  ex-sategoelelomsuc  32680  ex-sategoelel12  32681  dfrdg2  33047  sltval2  33170  nosgnn0  33172  sltintdifex  33175  sltres  33176  sltsolem1  33187  nolt02o  33206  dfrdg4  33419  bj-1nel0  34282  bj-pr21val  34341  finxpreclem2  34687  epnsymrel  35836  0dioph  39514  clsk1indlem1  40530  dirkercncflem2  42537  fourierdlem60  42599  fourierdlem61  42600  afv20defat  43579  fun2dmnopgexmpl  43631  itcoval1  44837  line2ylem  44925
  Copyright terms: Public domain W3C validator