Theorem neneqd 2423

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1397   =/= wne 2402

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 2403

This theorem is referenced by:  neneq  2424  necon2bi  2457  necon2i  2458  pm2.21ddne  2485  nelrdva  3013  neq0r  3509  ifnetruedc  3649  ifnefals  3650  0inp0  4256  pwntru  4289  nndceq0  4716  frecabcl  6565  frecsuclem  6572  nnsucsssuc  6660  phpm  7052  diffisn  7082  en2eqpr  7099  fival  7169  omp1eomlem  7293  difinfsnlem  7298  difinfsn  7299  ctmlemr  7307  nninfisollemne  7330  fodjuomnilemdc  7343  exmidapne  7479  indpi  7562  nqnq0pi  7658  ltxrlt  8245  sup3exmid  9137  elnnz  9489  xrnemnf  10012  xrnepnf  10013  xrlttri3  10032  nltpnft  10049  ngtmnft  10052  xrpnfdc  10077  xrmnfdc  10078  xleaddadd  10122  fzprval  10317  fzodisjsn  10419  xqltnle  10528  fxnn0nninf  10702  iseqf1olemklt  10761  seq3f1olemqsumkj  10774  expnnval  10805  fihashelne0d  11060  xrmaxrecl  11833  fsumcl2lem  11977  fprodcl2lem  12184  dvdsle  12423  mod2eq1n2dvds  12458  nndvdslegcd  12554  gcdnncl  12556  divgcdnn  12564  sqgcd  12618  eucalgf  12645  eucalginv  12646  lcmeq0  12661  lcmgcdlem  12667  qredeu  12687  rpdvds  12689  cncongr2  12694  divnumden  12786  divdenle  12787  phibndlem  12806  phisum  12831  oddprm  12850  pythagtriplem4  12859  pythagtriplem8  12863  pythagtriplem9  12864  pceq0  12913  4sqlem10  12978  ennnfonelemk  13039  ennnfonelemjn  13041  ennnfonelemp1  13045  ennnfonelemim  13063  mulgnn  13731  rrgnz  14301  aprirr  14316  isxmet2d  15091  dvexp2  15455  dvply1  15508  logbgcd1irraplemexp  15711  perfectlem2  15743  lgsval2lem  15758  lgsval4  15768  lgsdilem  15775  lgsdir  15783  gausslemma2dlem4  15812  lgseisenlem4  15821  lgsquadlem1  15825  lgsquad2  15831  m1lgs  15833  2sqlem8a  15870  2sqlem8  15871  uhgr2edg  16076  usgr1vr  16118  vdegp1aid  16184  g0wlk0  16240  eupth2lem2dc  16329  eupth2lem3lem6fi  16341  depindlem1  16376  pw1ndom3lem  16639  nnsf  16658  peano4nninf  16659  exmidsbthrlem  16677  refeq  16683  trilpolemeq1  16695  qdiff  16704  dceqnconst  16716