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

Theorem neii 2784
Description: Inference associated with df-ne 2782. (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 2782 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2mpbi 219 1 ¬ 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1475  wne 2780
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 196  df-ne 2782
This theorem is referenced by:  nesymi  2839  nemtbir  2877  snsssn  4312  2dom  7915  map2xp  8015  pm54.43lem  8708  canthp1lem2  9354  ine0  10344  inelr  10887  xrltnr  11829  pnfnlt  11838  prprrab  13112  wrdlen2i  13534  3lcm2e6woprm  15166  6lcm4e12  15167  m1dvdsndvds  15341  xpsfrnel2  16048  pmatcollpw3fi1lem1  20410  sinhalfpilem  24019  coseq1  24078  2lgslem3  24929  2lgslem4  24931  axlowdimlem13  25634  axlowdim1  25639  umgredgnlp  25818  usgraedgprv  25905  wlkntrllem3  26091  4cycl4dv  26195  wwlknext  26252  norm1exi  27491  largei  28510  ind1a  29410  ballotlemii  29892  sgnnbi  29934  sgnpbi  29935  dfrdg2  30945  sltval2  31053  nosgnn0  31055  sltintdifex  31060  sltres  31061  sltsolem1  31067  dfrdg4  31228  bj-1nel0  32134  bj-pr21val  32194  finxpreclem2  32403  0dioph  36360  clsk1indlem1  37363  dirkercncflem2  38997  fourierdlem60  39059  fourierdlem61  39060  fun2dmnopgexmpl  40329  uvtxa01vtx  40624  wwlksnext  41099
  Copyright terms: Public domain W3C validator