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  6420  ltxrlt  6862  elnnz  8011  xrnemnf  8449  xrnepnf  8450  xrlttri3  8468  nltpnft  8480  ngtmnft  8481  fzprval  8694  expival  8891  expinnval  8892
  Copyright terms: Public domain W3C validator