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 )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1402   =/= wne 2420

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 2421

This theorem is referenced by:  neneq  2442  necon2bi  2475  necon2i  2476  pm2.21ddne  2503  nelrdva  3033  neq0r  3536  ifnetruedc  3681  ifnefals  3682  0inp0  4298  pwntru  4331  nndceq0  4760  fczsupp0  6489  frecabcl  6660  frecsuclem  6667  nnsucsssuc  6755  phpm  7157  diffisn  7187  en2eqpr  7204  fival  7294  omp1eomlem  7424  difinfsnlem  7429  difinfsn  7430  ctmlemr  7438  nninfisollemne  7461  fodjuomnilemdc  7474  exmidapne  7616  indpi  7699  nqnq0pi  7795  ltxrlt  8381  sup3exmid  9277  elnnz  9633  xrnemnf  10158  xrnepnf  10159  xrlttri3  10178  nltpnft  10195  ngtmnft  10198  xrpnfdc  10223  xrmnfdc  10224  xleaddadd  10268  fzprval  10467  fzodisjsn  10569  xqltnle  10680  fxnn0nninf  10854  iseqf1olemklt  10913  seq3f1olemqsumkj  10926  expnnval  10957  fihashelne0d  11214  xrmaxrecl  11999  fsumcl2lem  12143  fprodcl2lem  12350  dvdsle  12589  mod2eq1n2dvds  12624  nndvdslegcd  12720  gcdnncl  12722  divgcdnn  12730  sqgcd  12784  eucalgf  12811  eucalginv  12812  lcmeq0  12827  lcmgcdlem  12833  qredeu  12853  rpdvds  12855  cncongr2  12860  divnumden  12952  divdenle  12953  phibndlem  12972  phisum  12997  oddprm  13016  pythagtriplem4  13025  pythagtriplem8  13029  pythagtriplem9  13030  pceq0  13079  4sqlem10  13144  ballotfilemirc  13253  ennnfonelemk  13269  ennnfonelemjn  13271  ennnfonelemp1  13275  ennnfonelemim  13293  mulgnn  13906  rrgnz  14550  aprirr  14568  isxmet2d  15372  dvexp2  15736  dvply1  15789  logbgcd1irraplemexp  15993  perfectlem2  16028  lgsval2lem  16043  lgsval4  16053  lgsdilem  16060  lgsdir  16068  gausslemma2dlem4  16097  lgseisenlem4  16106  lgsquadlem1  16110  lgsquad2  16116  m1lgs  16118  2sqlem8a  16155  2sqlem8  16156  uhgr2edg  16361  usgr1vr  16403  vdegp1aid  16469  g0wlk0  16525  eupth2lem2dc  16614  eupth2lem3lem6fi  16626  depindlem1  16661  dichmul0orlem5  16671  dichmul0orlem6  16672  pw1ndom3lem  16933  nnsf  16953  peano4nninf  16954  exmidsbthrlem  16972  refeq  16978  trilpolemeq1  16994  qdiff  17003  dceqnconst  17015