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  9287  elnnz  9654  xrnemnf  10179  xrnepnf  10180  xrlttri3  10199  nltpnft  10216  ngtmnft  10219  xrpnfdc  10244  xrmnfdc  10245  xleaddadd  10289  fzprval  10489  fzodisjsn  10591  xqltnle  10702  fxnn0nninf  10876  iseqf1olemklt  10935  seq3f1olemqsumkj  10948  expnnval  10979  fihashelne0d  11236  xrmaxrecl  12021  fsumcl2lem  12165  fprodcl2lem  12372  dvdsle  12611  mod2eq1n2dvds  12646  nndvdslegcd  12742  gcdnncl  12744  divgcdnn  12752  sqgcd  12806  eucalgf  12833  eucalginv  12834  lcmeq0  12849  lcmgcdlem  12855  qredeu  12875  rpdvds  12877  cncongr2  12882  divnumden  12974  divdenle  12975  phibndlem  12994  phisum  13019  oddprm  13038  pythagtriplem4  13047  pythagtriplem8  13051  pythagtriplem9  13052  pceq0  13101  4sqlem10  13166  ballotfilemirc  13275  ennnfonelemk  13291  ennnfonelemjn  13293  ennnfonelemp1  13297  ennnfonelemim  13315  mulgnn  13929  rrgnz  14577  aprirr  14595  isxmet2d  15449  dvexp2  15813  dvply1  15866  logbgcd1irraplemexp  16070  perfectlem2  16114  lgsval2lem  16129  lgsval4  16139  lgsdilem  16146  lgsdir  16154  gausslemma2dlem4  16183  lgseisenlem4  16192  lgsquadlem1  16196  lgsquad2  16202  m1lgs  16204  2sqlem8a  16241  2sqlem8  16242  uhgr2edg  16447  usgr1vr  16489  vdegp1aid  16555  g0wlk0  16611  eupth2lem2dc  16700  eupth2lem3lem6fi  16712  depindlem1  16747  dichmul0orlem5  16757  dichmul0orlem6  16758  pw1ndom3lem  17019  nnsf  17048  peano4nninf  17049  exmidsbthrlem  17067  refeq  17073  trilpolemeq1  17089  qdiff  17098  dceqnconst  17110