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

Theorem neii 3018
Description: Inference associated with df-ne 3017. (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 3017 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2mpbi 231 1 ¬ 𝐴 = 𝐵
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3   = wceq 1528  wne 3016
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 208  df-ne 3017
This theorem is referenced by:  nesymi  3073  nemtbir  3112  snsssn  4766  2dom  8571  map2xp  8676  updjudhcoinrg  9351  pm54.43lem  9417  canthp1lem2  10064  ine0  11064  inelr  11617  xrltnr  12504  pnfnlt  12513  prprrab  13821  wrdlen2i  14294  3lcm2e6woprm  15949  6lcm4e12  15950  m1dvdsndvds  16125  fnpr2ob  16821  fvprif  16824  pmatcollpw3fi1lem1  21324  sinhalfpilem  24978  coseq1  25039  2lgslem3  25908  2lgslem4  25910  axlowdimlem13  26668  axlowdim1  26673  umgredgnlp  26860  wwlksnext  27599  norm1exi  28955  largei  29972  ind1a  31178  ballotlemii  31661  sgnnbi  31703  sgnpbi  31704  gonanegoal  32497  gonan0  32537  goaln0  32538  fmlasucdisj  32544  ex-sategoelelomsuc  32571  ex-sategoelel12  32572  dfrdg2  32938  sltval2  33061  nosgnn0  33063  sltintdifex  33066  sltres  33067  sltsolem1  33078  nolt02o  33097  dfrdg4  33310  bj-1nel0  34164  bj-pr21val  34223  finxpreclem2  34554  epnsymrel  35680  0dioph  39255  clsk1indlem1  40275  dirkercncflem2  42270  fourierdlem60  42332  fourierdlem61  42333  afv20defat  43312  fun2dmnopgexmpl  43364  line2ylem  44636
  Copyright terms: Public domain W3C validator