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  16198  lgsval2lem  16227  lgsval4  16237  lgsdilem  16244  lgsdir  16252  gausslemma2dlem4  16281  lgseisenlem4  16290  lgsquadlem1  16294  lgsquad2  16300  m1lgs  16302  2sqlem8a  16339  2sqlem8  16340  uhgr2edg  16545  usgr1vr  16587  vdegp1aid  16653  g0wlk0  16709  eupth2lem2dc  16798  eupth2lem3lem6fi  16810  depindlem1  16845  dichmul0orlem5  16855  dichmul0orlem6  16856  pw1ndom3lem  17117  nnsf  17146  peano4nninf  17147  exmidsbthrlem  17165  refeq  17171  trilpolemeq1  17187  qdiff  17196  dceqnconst  17208