ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  neneqd Structured version   GIF version

Theorem neneqd 2221
Description: Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
neneqd.1 (φAB)
Assertion
Ref Expression
neneqd (φ → ¬ A = B)

Proof of Theorem neneqd
StepHypRef Expression
1 neneqd.1 . 2 (φAB)
2 df-ne 2203 . 2 (AB ↔ ¬ A = B)
31, 2sylib 127 1 (φ → ¬ A = B)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1242  wne 2201
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110  df-ne 2203
This theorem is referenced by:  necon2bi  2254  necon2i  2255  pm2.21ddne  2282  nelrdva  2740  neq0r  3229  0inp0  3910  nndceq0  4282  frecsuclem3  5929  nnsucsssuc  6010  indpi  6326  nqnq0pi  6421  ltxrlt  6882  elnnz  8031  xrnemnf  8469  xrnepnf  8470  xrlttri3  8488  nltpnft  8500  ngtmnft  8501  fzprval  8714  expival  8911  expinnval  8912
  Copyright terms: Public domain W3C validator