Theorem neneqd 2441

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

This proof depends on syntax axioms:   -. wn 3   -> wi 4   = wceq 1402   =/= wne 2420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117  df-ne 2421

This theorem is used by:  neneq  2442  necon2bi  2475  necon2i  2476  pm2.21ddne  2503  nelrdva  3033  neq0r  3536  ifnetruedc  3684  ifnefals  3685  0inp0  4303  pwntru  4336  nndceq0  4765  fczsupp0  6499  frecabcl  6670  frecsuclem  6677  nnsucsssuc  6765  phpm  7167  diffisn  7197  en2eqpr  7214  fival  7304  omp1eomlem  7434  difinfsnlem  7439  difinfsn  7440  ctmlemr  7448  nninfisollemne  7471  fodjuomnilemdc  7484  exmidapne  7626  indpi  7709  nqnq0pi  7805  ltxrlt  8391  sup3exmid  9289  elnnz  9658  xrnemnf  10189  xrnepnf  10190  xrlttri3  10209  nltpnft  10226  ngtmnft  10229  xrpnfdc  10254  xrmnfdc  10255  xleaddadd  10299  fzprval  10499  fzodisjsn  10601  xqltnle  10712  fxnn0nninf  10889  iseqf1olemklt  10948  seq3f1olemqsumkj  10961  expnnval  10992  fihashelne0d  11250  xrmaxrecl  12037  fsumcl2lem  12181  fprodcl2lem  12388  dvdsle  12627  mod2eq1n2dvds  12662  nndvdslegcd  12758  gcdnncl  12760  divgcdnn  12768  sqgcd  12822  eucalgf  12849  eucalginv  12850  lcmeq0  12865  lcmgcdlem  12871  qredeu  12891  rpdvds  12893  cncongr2  12898  divnumden  12992  divdenle  12993  phibndlem  13014  phisum  13039  oddprm  13058  pythagtriplem4  13067  pythagtriplem8  13071  pythagtriplem9  13072  pceq0  13121  4sqlem10  13186  ballotfilemirc  13324  ennnfonelemk  13340  ennnfonelemjn  13342  ennnfonelemp1  13346  ennnfonelemim  13364  mulgnn  13978  rrgnz  14626  aprirr  14644  isxmet2d  15498  dvexp2  15862  dvply1  15915  logbgcd1irraplemexp  16123  perfectlem2  16219  lgsval2lem  16248  lgsval4  16258  lgsdilem  16265  lgsdir  16273  gausslemma2dlem4  16302  lgseisenlem4  16311  lgsquadlem1  16315  lgsquad2  16321  m1lgs  16323  2sqlem8a  16360  2sqlem8  16361  uhgr2edg  16566  usgr1vr  16608  vdegp1aid  16674  g0wlk0  16730  eupth2lem2dc  16819  eupth2lem3lem6fi  16831  depindlem1  16866  dichmul0orlem5  16876  dichmul0orlem6  16877  pw1ndom3lem  17138  nnsf  17167  peano4nninf  17168  exmidsbthrlem  17186  refeq  17192  trilpolemeq1  17208  qdiff  17217  dceqnconst  17229