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

Theorem neii 2688
 Description: Inference associated with df-ne 2686. (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 2686 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2mpbi 218 1 ¬ 𝐴 = 𝐵
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   = wceq 1474   ≠ wne 2684 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 195  df-ne 2686 This theorem is referenced by:  nesymi  2743  nemtbir  2781  snsssn  4211  2dom  7791  map2xp  7891  pm54.43lem  8584  canthp1lem2  9230  ine0  10216  inelr  10765  xrltnr  11700  pnfnlt  11709  wrdlen2i  13393  3lcm2e6woprm  15042  6lcm4e12  15043  m1dvdsndvds  15225  xpsfrnel2  15940  pmatcollpw3fi1lem1  20313  sinhalfpilem  23906  coseq1  23965  2lgslem3  24818  2lgslem4  24820  axlowdimlem13  25524  axlowdim1  25529  usgraedgprv  25643  wlkntrllem3  25829  4cycl4dv  25933  wwlknext  25990  vcoprne  26572  norm1exi  27279  largei  28298  ind1a  29206  ballotlemii  29699  ballotlemiiOLD  29737  sgnnbi  29779  sgnpbi  29780  dfrdg2  30787  sltval2  30888  nosgnn0  30890  sltintdifex  30895  sltres  30896  sltsolem1  30902  dfrdg4  31063  bj-1nel0  31965  bj-pr21val  32025  finxpreclem2  32234  0dioph  36250  clsk1indlem1  37260  dirkercncflem2  38900  fourierdlem60  38964  fourierdlem61  38965  fun2dmnopgexmpl  40259  prprrab  40300  umgredgnlp  40482  uvtxa01vtx  40729  wwlksnext  41204
 Copyright terms: Public domain W3C validator