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

Theorem neneqd 2276
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 2256 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylib 120 1 (𝜑 → ¬ 𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1289  wne 2255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104
This theorem depends on definitions:  df-bi 115  df-ne 2256
This theorem is referenced by:  neneq  2277  necon2bi  2310  necon2i  2311  pm2.21ddne  2338  nelrdva  2820  neq0r  3295  0inp0  3993  nndceq0  4421  frecabcl  6146  frecsuclem  6153  nnsucsssuc  6235  phpm  6561  diffisn  6589  en2eqpr  6603  fodjuomnilemdc  6778  indpi  6880  nqnq0pi  6976  ltxrlt  7531  elnnz  8730  xrnemnf  9217  xrnepnf  9218  xrlttri3  9236  nltpnft  9248  ngtmnft  9249  fzprval  9463  fxnn0nninf  9809  iseqf1olemklt  9879  seq3f1olemqsumkj  9892  expnnval  9923  fsumcl2lem  10755  dvdsle  10938  mod2eq1n2dvds  10972  nndvdslegcd  11050  gcdnncl  11052  divgcdnn  11059  sqgcd  11111  eucalgf  11130  eucalginv  11131  lcmeq0  11146  lcmgcdlem  11152  qredeu  11172  rpdvds  11174  cncongr2  11179  divnumden  11267  divdenle  11268  phibndlem  11285  nnsf  11552  peano4nninf  11553  exmidsbthrlem  11569
  Copyright terms: Public domain W3C validator