Theorem neneqd 2366

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 2346	. 2 |- ( A =/= B <-> -. A = B )
3	1, 2	sylib 122	1 |- ( ph -> -. A = B )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1353   =/= wne 2345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117  df-ne 2346

This theorem is referenced by:  neneq  2367  necon2bi  2400  necon2i  2401  pm2.21ddne  2428  nelrdva  2942  neq0r  3435  0inp0  4161  pwntru  4194  nndceq0  4611  frecabcl  6390  frecsuclem  6397  nnsucsssuc  6483  phpm  6855  diffisn  6883  en2eqpr  6897  fival  6959  omp1eomlem  7083  difinfsnlem  7088  difinfsn  7089  ctmlemr  7097  nninfisollemne  7119  fodjuomnilemdc  7132  indpi  7316  nqnq0pi  7412  ltxrlt  7997  sup3exmid  8887  elnnz  9236  xrnemnf  9748  xrnepnf  9749  xrlttri3  9768  nltpnft  9785  ngtmnft  9788  xrpnfdc  9813  xrmnfdc  9814  xleaddadd  9858  fzprval  10052  fxnn0nninf  10408  iseqf1olemklt  10455  seq3f1olemqsumkj  10468  expnnval  10493  fihashelne0d  10745  xrmaxrecl  11231  fsumcl2lem  11374  fprodcl2lem  11581  dvdsle  11817  mod2eq1n2dvds  11851  nndvdslegcd  11933  gcdnncl  11935  divgcdnn  11943  sqgcd  11997  eucalgf  12022  eucalginv  12023  lcmeq0  12038  lcmgcdlem  12044  qredeu  12064  rpdvds  12066  cncongr2  12071  divnumden  12163  divdenle  12164  phibndlem  12183  phisum  12207  oddprm  12226  pythagtriplem4  12235  pythagtriplem8  12239  pythagtriplem9  12240  pceq0  12288  4sqlem10  12352  ennnfonelemk  12368  ennnfonelemjn  12370  ennnfonelemp1  12374  ennnfonelemim  12392  mulgnn  12850  isxmet2d  13419  dvexp2  13747  logbgcd1irraplemexp  13957  lgsval2lem  13982  lgsval4  13992  lgsdilem  13999  lgsdir  14007  2sqlem8a  14029  2sqlem8  14030  nnsf  14315  peano4nninf  14316  exmidsbthrlem  14331  refeq  14337  trilpolemeq1  14349  dceqnconst  14368