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

Theorem neneqd 2241
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 2221 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylib 131 1 (𝜑 → ¬ 𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1259  wne 2220
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103
This theorem depends on definitions:  df-bi 114  df-ne 2221
This theorem is referenced by:  neneq  2242  necon2bi  2275  necon2i  2276  pm2.21ddne  2303  nelrdva  2769  neq0r  3263  0inp0  3947  nndceq0  4367  frecsuclem3  6021  nnsucsssuc  6102  phpm  6358  diffisn  6381  indpi  6498  nqnq0pi  6594  ltxrlt  7144  elnnz  8312  xrnemnf  8800  xrnepnf  8801  xrlttri3  8819  nltpnft  8831  ngtmnft  8832  fzprval  9046  expival  9422  expinnval  9423  dvdsle  10156  mod2eq1n2dvds  10191
  Copyright terms: Public domain W3C validator