Theorem neneqd 2424

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1398   =/= wne 2403

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 2404

This theorem is referenced by:  neneq  2425  necon2bi  2458  necon2i  2459  pm2.21ddne  2486  nelrdva  3014  neq0r  3511  ifnetruedc  3653  ifnefals  3654  0inp0  4262  pwntru  4295  nndceq0  4722  fczsupp0  6437  frecabcl  6608  frecsuclem  6615  nnsucsssuc  6703  phpm  7095  diffisn  7125  en2eqpr  7142  fival  7229  omp1eomlem  7353  difinfsnlem  7358  difinfsn  7359  ctmlemr  7367  nninfisollemne  7390  fodjuomnilemdc  7403  exmidapne  7539  indpi  7622  nqnq0pi  7718  ltxrlt  8304  sup3exmid  9196  elnnz  9550  xrnemnf  10073  xrnepnf  10074  xrlttri3  10093  nltpnft  10110  ngtmnft  10113  xrpnfdc  10138  xrmnfdc  10139  xleaddadd  10183  fzprval  10379  fzodisjsn  10481  xqltnle  10590  fxnn0nninf  10764  iseqf1olemklt  10823  seq3f1olemqsumkj  10836  expnnval  10867  fihashelne0d  11122  xrmaxrecl  11895  fsumcl2lem  12039  fprodcl2lem  12246  dvdsle  12485  mod2eq1n2dvds  12520  nndvdslegcd  12616  gcdnncl  12618  divgcdnn  12626  sqgcd  12680  eucalgf  12707  eucalginv  12708  lcmeq0  12723  lcmgcdlem  12729  qredeu  12749  rpdvds  12751  cncongr2  12756  divnumden  12848  divdenle  12849  phibndlem  12868  phisum  12893  oddprm  12912  pythagtriplem4  12921  pythagtriplem8  12925  pythagtriplem9  12926  pceq0  12975  4sqlem10  13040  ennnfonelemk  13101  ennnfonelemjn  13103  ennnfonelemp1  13107  ennnfonelemim  13125  mulgnn  13793  rrgnz  14364  aprirr  14379  isxmet2d  15159  dvexp2  15523  dvply1  15576  logbgcd1irraplemexp  15779  perfectlem2  15814  lgsval2lem  15829  lgsval4  15839  lgsdilem  15846  lgsdir  15854  gausslemma2dlem4  15883  lgseisenlem4  15892  lgsquadlem1  15896  lgsquad2  15902  m1lgs  15904  2sqlem8a  15941  2sqlem8  15942  uhgr2edg  16147  usgr1vr  16189  vdegp1aid  16255  g0wlk0  16311  eupth2lem2dc  16400  eupth2lem3lem6fi  16412  depindlem1  16447  pw1ndom3lem  16709  nnsf  16731  peano4nninf  16732  exmidsbthrlem  16750  refeq  16756  trilpolemeq1  16772  qdiff  16781  dceqnconst  16793