Theorem neneqd 2421

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1395   =/= wne 2400

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 2401

This theorem is referenced by:  neneq  2422  necon2bi  2455  necon2i  2456  pm2.21ddne  2483  nelrdva  3011  neq0r  3507  ifnetruedc  3647  ifnefals  3648  0inp0  4252  pwntru  4285  nndceq0  4712  frecabcl  6558  frecsuclem  6565  nnsucsssuc  6653  phpm  7045  diffisn  7073  en2eqpr  7090  fival  7158  omp1eomlem  7282  difinfsnlem  7287  difinfsn  7288  ctmlemr  7296  nninfisollemne  7319  fodjuomnilemdc  7332  exmidapne  7467  indpi  7550  nqnq0pi  7646  ltxrlt  8233  sup3exmid  9125  elnnz  9477  xrnemnf  10000  xrnepnf  10001  xrlttri3  10020  nltpnft  10037  ngtmnft  10040  xrpnfdc  10065  xrmnfdc  10066  xleaddadd  10110  fzprval  10305  fzodisjsn  10407  xqltnle  10515  fxnn0nninf  10689  iseqf1olemklt  10748  seq3f1olemqsumkj  10761  expnnval  10792  fihashelne0d  11047  xrmaxrecl  11803  fsumcl2lem  11946  fprodcl2lem  12153  dvdsle  12392  mod2eq1n2dvds  12427  nndvdslegcd  12523  gcdnncl  12525  divgcdnn  12533  sqgcd  12587  eucalgf  12614  eucalginv  12615  lcmeq0  12630  lcmgcdlem  12636  qredeu  12656  rpdvds  12658  cncongr2  12663  divnumden  12755  divdenle  12756  phibndlem  12775  phisum  12800  oddprm  12819  pythagtriplem4  12828  pythagtriplem8  12832  pythagtriplem9  12833  pceq0  12882  4sqlem10  12947  ennnfonelemk  13008  ennnfonelemjn  13010  ennnfonelemp1  13014  ennnfonelemim  13032  mulgnn  13700  rrgnz  14269  aprirr  14284  isxmet2d  15059  dvexp2  15423  dvply1  15476  logbgcd1irraplemexp  15679  perfectlem2  15711  lgsval2lem  15726  lgsval4  15736  lgsdilem  15743  lgsdir  15751  gausslemma2dlem4  15780  lgseisenlem4  15789  lgsquadlem1  15793  lgsquad2  15799  m1lgs  15801  2sqlem8a  15838  2sqlem8  15839  uhgr2edg  16041  usgr1vr  16083  g0wlk0  16158  pw1ndom3lem  16498  nnsf  16517  peano4nninf  16518  exmidsbthrlem  16536  refeq  16542  trilpolemeq1  16554  dceqnconst  16574