Theorem neneqd 2399

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1373   =/= wne 2378

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 2379

This theorem is referenced by:  neneq  2400  necon2bi  2433  necon2i  2434  pm2.21ddne  2461  nelrdva  2987  neq0r  3483  ifnetruedc  3623  ifnefals  3624  0inp0  4226  pwntru  4259  nndceq0  4684  frecabcl  6508  frecsuclem  6515  nnsucsssuc  6601  phpm  6988  diffisn  7016  en2eqpr  7030  fival  7098  omp1eomlem  7222  difinfsnlem  7227  difinfsn  7228  ctmlemr  7236  nninfisollemne  7259  fodjuomnilemdc  7272  exmidapne  7407  indpi  7490  nqnq0pi  7586  ltxrlt  8173  sup3exmid  9065  elnnz  9417  xrnemnf  9934  xrnepnf  9935  xrlttri3  9954  nltpnft  9971  ngtmnft  9974  xrpnfdc  9999  xrmnfdc  10000  xleaddadd  10044  fzprval  10239  fzodisjsn  10341  xqltnle  10447  fxnn0nninf  10621  iseqf1olemklt  10680  seq3f1olemqsumkj  10693  expnnval  10724  fihashelne0d  10979  xrmaxrecl  11681  fsumcl2lem  11824  fprodcl2lem  12031  dvdsle  12270  mod2eq1n2dvds  12305  nndvdslegcd  12401  gcdnncl  12403  divgcdnn  12411  sqgcd  12465  eucalgf  12492  eucalginv  12493  lcmeq0  12508  lcmgcdlem  12514  qredeu  12534  rpdvds  12536  cncongr2  12541  divnumden  12633  divdenle  12634  phibndlem  12653  phisum  12678  oddprm  12697  pythagtriplem4  12706  pythagtriplem8  12710  pythagtriplem9  12711  pceq0  12760  4sqlem10  12825  ennnfonelemk  12886  ennnfonelemjn  12888  ennnfonelemp1  12892  ennnfonelemim  12910  mulgnn  13577  rrgnz  14145  aprirr  14160  isxmet2d  14935  dvexp2  15299  dvply1  15352  logbgcd1irraplemexp  15555  perfectlem2  15587  lgsval2lem  15602  lgsval4  15612  lgsdilem  15619  lgsdir  15627  gausslemma2dlem4  15656  lgseisenlem4  15665  lgsquadlem1  15669  lgsquad2  15675  m1lgs  15677  2sqlem8a  15714  2sqlem8  15715  nnsf  16144  peano4nninf  16145  exmidsbthrlem  16163  refeq  16169  trilpolemeq1  16181  dceqnconst  16201