Theorem neneqd 2303

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1314   =/= wne 2282

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

This theorem depends on definitions:  df-bi 116  df-ne 2283

This theorem is referenced by:  neneq  2304  necon2bi  2337  necon2i  2338  pm2.21ddne  2365  nelrdva  2860  neq0r  3343  0inp0  4050  pwntru  4082  nndceq0  4491  frecabcl  6250  frecsuclem  6257  nnsucsssuc  6342  phpm  6712  diffisn  6740  en2eqpr  6754  fival  6810  omp1eomlem  6931  difinfsnlem  6936  difinfsn  6937  ctmlemr  6945  fodjuomnilemdc  6966  indpi  7098  nqnq0pi  7194  ltxrlt  7754  sup3exmid  8625  elnnz  8968  xrnemnf  9457  xrnepnf  9458  xrlttri3  9476  nltpnft  9490  ngtmnft  9493  xrpnfdc  9518  xrmnfdc  9519  xleaddadd  9563  fzprval  9755  fxnn0nninf  10104  iseqf1olemklt  10151  seq3f1olemqsumkj  10164  expnnval  10189  xrmaxrecl  10916  fsumcl2lem  11059  dvdsle  11390  mod2eq1n2dvds  11424  nndvdslegcd  11502  gcdnncl  11504  divgcdnn  11511  sqgcd  11563  eucalgf  11582  eucalginv  11583  lcmeq0  11598  lcmgcdlem  11604  qredeu  11624  rpdvds  11626  cncongr2  11631  divnumden  11719  divdenle  11720  phibndlem  11737  ennnfonelemk  11758  ennnfonelemjn  11760  ennnfonelemp1  11764  ennnfonelemim  11782  isxmet2d  12337  nnsf  12891  peano4nninf  12892  exmidsbthrlem  12909  refeq  12915  trilpolemeq1  12925