Theorem neneqd 2388

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1364   =/= wne 2367

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 2368

This theorem is referenced by:  neneq  2389  necon2bi  2422  necon2i  2423  pm2.21ddne  2450  nelrdva  2971  neq0r  3466  ifnetruedc  3603  ifnefals  3604  0inp0  4200  pwntru  4233  nndceq0  4655  frecabcl  6466  frecsuclem  6473  nnsucsssuc  6559  phpm  6935  diffisn  6963  en2eqpr  6977  fival  7045  omp1eomlem  7169  difinfsnlem  7174  difinfsn  7175  ctmlemr  7183  nninfisollemne  7206  fodjuomnilemdc  7219  exmidapne  7343  indpi  7426  nqnq0pi  7522  ltxrlt  8109  sup3exmid  9001  elnnz  9353  xrnemnf  9869  xrnepnf  9870  xrlttri3  9889  nltpnft  9906  ngtmnft  9909  xrpnfdc  9934  xrmnfdc  9935  xleaddadd  9979  fzprval  10174  xqltnle  10374  fxnn0nninf  10548  iseqf1olemklt  10607  seq3f1olemqsumkj  10620  expnnval  10651  fihashelne0d  10906  xrmaxrecl  11437  fsumcl2lem  11580  fprodcl2lem  11787  dvdsle  12026  mod2eq1n2dvds  12061  nndvdslegcd  12157  gcdnncl  12159  divgcdnn  12167  sqgcd  12221  eucalgf  12248  eucalginv  12249  lcmeq0  12264  lcmgcdlem  12270  qredeu  12290  rpdvds  12292  cncongr2  12297  divnumden  12389  divdenle  12390  phibndlem  12409  phisum  12434  oddprm  12453  pythagtriplem4  12462  pythagtriplem8  12466  pythagtriplem9  12467  pceq0  12516  4sqlem10  12581  ennnfonelemk  12642  ennnfonelemjn  12644  ennnfonelemp1  12648  ennnfonelemim  12666  mulgnn  13332  rrgnz  13900  aprirr  13915  isxmet2d  14668  dvexp2  15032  dvply1  15085  logbgcd1irraplemexp  15288  perfectlem2  15320  lgsval2lem  15335  lgsval4  15345  lgsdilem  15352  lgsdir  15360  gausslemma2dlem4  15389  lgseisenlem4  15398  lgsquadlem1  15402  lgsquad2  15408  m1lgs  15410  2sqlem8a  15447  2sqlem8  15448  nnsf  15736  peano4nninf  15737  exmidsbthrlem  15753  refeq  15759  trilpolemeq1  15771  dceqnconst  15791