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

Theorem neneqd 2226
 Description: Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
neneqd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
neneqd (𝜑 → ¬ 𝐴 = 𝐵)

Proof of Theorem neneqd
StepHypRef Expression
1 neneqd.1 . 2 (𝜑𝐴𝐵)
2 df-ne 2206 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylib 127 1 (𝜑 → ¬ 𝐴 = 𝐵)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1243   ≠ wne 2204 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 2206 This theorem is referenced by:  neneq  2227  necon2bi  2260  necon2i  2261  pm2.21ddne  2288  nelrdva  2746  neq0r  3235  0inp0  3919  nndceq0  4339  frecsuclem3  5990  nnsucsssuc  6071  phpm  6327  diffisn  6350  indpi  6440  nqnq0pi  6536  ltxrlt  7085  elnnz  8255  xrnemnf  8699  xrnepnf  8700  xrlttri3  8718  nltpnft  8730  ngtmnft  8731  fzprval  8944  expival  9257  expinnval  9258
 Copyright terms: Public domain W3C validator