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

Theorem neii 2934
Description: Inference associated with df-ne 2933. (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 2933 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2mpbi 220 1 ¬ 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1632  wne 2932
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 2933
This theorem is referenced by:  nesymi  2989  nemtbir  3027  snsssn  4517  2dom  8196  map2xp  8297  updjudhcoinrg  8969  pm54.43lem  9035  canthp1lem2  9687  ine0  10677  inelr  11222  xrltnr  12166  pnfnlt  12175  prprrab  13467  wrdlen2i  13907  3lcm2e6woprm  15550  6lcm4e12  15551  m1dvdsndvds  15725  xpsfrnel2  16447  pmatcollpw3fi1lem1  20813  sinhalfpilem  24435  coseq1  24494  2lgslem3  25349  2lgslem4  25351  axlowdimlem13  26054  axlowdim1  26059  umgredgnlp  26262  wwlksnext  27032  norm1exi  28437  largei  29456  ind1a  30411  ballotlemii  30895  sgnnbi  30937  sgnpbi  30938  dfrdg2  32027  sltval2  32136  nosgnn0  32138  sltintdifex  32141  sltres  32142  sltsolem1  32153  nolt02o  32172  dfrdg4  32385  bj-1nel0  33265  bj-pr21val  33325  finxpreclem2  33556  epnsymrel  34649  0dioph  37862  clsk1indlem1  38863  dirkercncflem2  40842  fourierdlem60  40904  fourierdlem61  40905  fun2dmnopgexmpl  41829
  Copyright terms: Public domain W3C validator