Theorem neneqd 2435

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

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

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 2415

This theorem is referenced by:  neneq  2436  necon2bi  2469  necon2i  2470  pm2.21ddne  2497  nelrdva  3027  neq0r  3527  ifnetruedc  3670  ifnefals  3671  0inp0  4284  pwntru  4317  nndceq0  4745  fczsupp0  6472  frecabcl  6643  frecsuclem  6650  nnsucsssuc  6738  phpm  7133  diffisn  7163  en2eqpr  7180  fival  7270  omp1eomlem  7398  difinfsnlem  7403  difinfsn  7404  ctmlemr  7412  nninfisollemne  7435  fodjuomnilemdc  7448  exmidapne  7590  indpi  7673  nqnq0pi  7769  ltxrlt  8355  sup3exmid  9248  elnnz  9604  xrnemnf  10129  xrnepnf  10130  xrlttri3  10149  nltpnft  10166  ngtmnft  10169  xrpnfdc  10194  xrmnfdc  10195  xleaddadd  10239  fzprval  10438  fzodisjsn  10540  xqltnle  10651  fxnn0nninf  10825  iseqf1olemklt  10884  seq3f1olemqsumkj  10897  expnnval  10928  fihashelne0d  11185  xrmaxrecl  11965  fsumcl2lem  12109  fprodcl2lem  12316  dvdsle  12555  mod2eq1n2dvds  12590  nndvdslegcd  12686  gcdnncl  12688  divgcdnn  12696  sqgcd  12750  eucalgf  12777  eucalginv  12778  lcmeq0  12793  lcmgcdlem  12799  qredeu  12819  rpdvds  12821  cncongr2  12826  divnumden  12918  divdenle  12919  phibndlem  12938  phisum  12963  oddprm  12982  pythagtriplem4  12991  pythagtriplem8  12995  pythagtriplem9  12996  pceq0  13045  4sqlem10  13110  ballotfilemirc  13219  ennnfonelemk  13235  ennnfonelemjn  13237  ennnfonelemp1  13241  ennnfonelemim  13259  mulgnn  13879  rrgnz  14515  aprirr  14533  isxmet2d  15339  dvexp2  15703  dvply1  15756  logbgcd1irraplemexp  15959  perfectlem2  15994  lgsval2lem  16009  lgsval4  16019  lgsdilem  16026  lgsdir  16034  gausslemma2dlem4  16063  lgseisenlem4  16072  lgsquadlem1  16076  lgsquad2  16082  m1lgs  16084  2sqlem8a  16121  2sqlem8  16122  uhgr2edg  16327  usgr1vr  16369  vdegp1aid  16435  g0wlk0  16491  eupth2lem2dc  16580  eupth2lem3lem6fi  16592  depindlem1  16627  pw1ndom3lem  16889  nnsf  16909  peano4nninf  16910  exmidsbthrlem  16928  refeq  16934  trilpolemeq1  16950  qdiff  16959  dceqnconst  16972