Theorem neneqd 2357

Description: Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
neneqd.1	|- ( ph -> A =/= B )

Assertion

Ref	Expression
neneqd	|- ( ph -> -. A = B )

Proof of Theorem neneqd

Step	Hyp	Ref	Expression
1		neneqd.1	. 2 |- ( ph -> A =/= B )
2		df-ne 2337	. 2 |- ( A =/= B <-> -. A = B )
3	1, 2	sylib 121	1 |- ( ph -> -. A = B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1343   =/= wne 2336

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 2337

This theorem is referenced by:  neneq  2358  necon2bi  2391  necon2i  2392  pm2.21ddne  2419  nelrdva  2933  neq0r  3423  0inp0  4145  pwntru  4178  nndceq0  4595  frecabcl  6367  frecsuclem  6374  nnsucsssuc  6460  phpm  6831  diffisn  6859  en2eqpr  6873  fival  6935  omp1eomlem  7059  difinfsnlem  7064  difinfsn  7065  ctmlemr  7073  nninfisollemne  7095  fodjuomnilemdc  7108  indpi  7283  nqnq0pi  7379  ltxrlt  7964  sup3exmid  8852  elnnz  9201  xrnemnf  9713  xrnepnf  9714  xrlttri3  9733  nltpnft  9750  ngtmnft  9753  xrpnfdc  9778  xrmnfdc  9779  xleaddadd  9823  fzprval  10017  fxnn0nninf  10373  iseqf1olemklt  10420  seq3f1olemqsumkj  10433  expnnval  10458  xrmaxrecl  11196  fsumcl2lem  11339  fprodcl2lem  11546  dvdsle  11782  mod2eq1n2dvds  11816  nndvdslegcd  11898  gcdnncl  11900  divgcdnn  11908  sqgcd  11962  eucalgf  11987  eucalginv  11988  lcmeq0  12003  lcmgcdlem  12009  qredeu  12029  rpdvds  12031  cncongr2  12036  divnumden  12128  divdenle  12129  phibndlem  12148  phisum  12172  oddprm  12191  pythagtriplem4  12200  pythagtriplem8  12204  pythagtriplem9  12205  pceq0  12253  4sqlem10  12317  ennnfonelemk  12333  ennnfonelemjn  12335  ennnfonelemp1  12339  ennnfonelemim  12357  isxmet2d  12998  dvexp2  13326  logbgcd1irraplemexp  13536  lgsval2lem  13561  lgsval4  13571  lgsdilem  13578  lgsdir  13586  2sqlem8a  13608  2sqlem8  13609  nnsf  13895  peano4nninf  13896  exmidsbthrlem  13911  refeq  13917  trilpolemeq1  13929  dceqnconst  13948