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

Theorem neneqd 2330
 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 2310 . 2
31, 2sylib 121 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wceq 1332   wne 2309 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105 This theorem depends on definitions:  df-bi 116  df-ne 2310 This theorem is referenced by:  neneq  2331  necon2bi  2364  necon2i  2365  pm2.21ddne  2392  nelrdva  2896  neq0r  3383  0inp0  4099  pwntru  4131  nndceq0  4540  frecabcl  6305  frecsuclem  6312  nnsucsssuc  6397  phpm  6768  diffisn  6796  en2eqpr  6810  fival  6868  omp1eomlem  6989  difinfsnlem  6994  difinfsn  6995  ctmlemr  7003  fodjuomnilemdc  7026  indpi  7194  nqnq0pi  7290  ltxrlt  7874  sup3exmid  8759  elnnz  9108  xrnemnf  9614  xrnepnf  9615  xrlttri3  9633  nltpnft  9647  ngtmnft  9650  xrpnfdc  9675  xrmnfdc  9676  xleaddadd  9720  fzprval  9913  fxnn0nninf  10262  iseqf1olemklt  10309  seq3f1olemqsumkj  10322  expnnval  10347  xrmaxrecl  11076  fsumcl2lem  11219  dvdsle  11598  mod2eq1n2dvds  11632  nndvdslegcd  11710  gcdnncl  11712  divgcdnn  11719  sqgcd  11773  eucalgf  11792  eucalginv  11793  lcmeq0  11808  lcmgcdlem  11814  qredeu  11834  rpdvds  11836  cncongr2  11841  divnumden  11930  divdenle  11931  phibndlem  11948  ennnfonelemk  11969  ennnfonelemjn  11971  ennnfonelemp1  11975  ennnfonelemim  11993  isxmet2d  12576  dvexp2  12904  logbgcd1irraplemexp  13113  nnsf  13393  peano4nninf  13394  exmidsbthrlem  13411  refeq  13417  trilpolemeq1  13429  dceqnconst  13448
 Copyright terms: Public domain W3C validator