Theorem neneqd 2385

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

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

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 2365

This theorem is referenced by:  neneq  2386  necon2bi  2419  necon2i  2420  pm2.21ddne  2447  nelrdva  2967  neq0r  3461  ifnetruedc  3598  ifnefals  3599  0inp0  4195  pwntru  4228  nndceq0  4650  frecabcl  6452  frecsuclem  6459  nnsucsssuc  6545  phpm  6921  diffisn  6949  en2eqpr  6963  fival  7029  omp1eomlem  7153  difinfsnlem  7158  difinfsn  7159  ctmlemr  7167  nninfisollemne  7190  fodjuomnilemdc  7203  exmidapne  7320  indpi  7402  nqnq0pi  7498  ltxrlt  8085  sup3exmid  8976  elnnz  9327  xrnemnf  9843  xrnepnf  9844  xrlttri3  9863  nltpnft  9880  ngtmnft  9883  xrpnfdc  9908  xrmnfdc  9909  xleaddadd  9953  fzprval  10148  xqltnle  10336  fxnn0nninf  10510  iseqf1olemklt  10569  seq3f1olemqsumkj  10582  expnnval  10613  fihashelne0d  10868  xrmaxrecl  11398  fsumcl2lem  11541  fprodcl2lem  11748  dvdsle  11986  mod2eq1n2dvds  12020  nndvdslegcd  12102  gcdnncl  12104  divgcdnn  12112  sqgcd  12166  eucalgf  12193  eucalginv  12194  lcmeq0  12209  lcmgcdlem  12215  qredeu  12235  rpdvds  12237  cncongr2  12242  divnumden  12334  divdenle  12335  phibndlem  12354  phisum  12378  oddprm  12397  pythagtriplem4  12406  pythagtriplem8  12410  pythagtriplem9  12411  pceq0  12460  4sqlem10  12525  ennnfonelemk  12557  ennnfonelemjn  12559  ennnfonelemp1  12563  ennnfonelemim  12581  mulgnn  13196  rrgnz  13764  aprirr  13779  isxmet2d  14516  dvexp2  14861  logbgcd1irraplemexp  15100  lgsval2lem  15126  lgsval4  15136  lgsdilem  15143  lgsdir  15151  gausslemma2dlem4  15180  lgseisenlem4  15189  lgsquadlem1  15191  m1lgs  15192  2sqlem8a  15209  2sqlem8  15210  nnsf  15495  peano4nninf  15496  exmidsbthrlem  15512  refeq  15518  trilpolemeq1  15530  dceqnconst  15550