Theorem neneqd 2799

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-ne 2795

This theorem is referenced by:  neneq  2800  necon2bi  2824  necon2i  2828  necon4i  2829  pm2.21ddne  2878  nelrdva  3417  disjprg  4648  0inp0  4837  onnseq  7441  sniffsupp  8315  ackbij1lem15  9056  ttukeylem7  9337  fpwwe2lem13  9464  canthnumlem  9470  canthp1lem2  9475  recgt0  10867  elnnz  11387  xrnemnf  11951  xrnepnf  11952  fzprval  12401  fzodisjsn  12505  expnnval  12863  elprchashprn2  13184  relexpsucnnr  13765  relexp1g  13766  relexpuzrel  13792  sgnp  13830  fprodn0f  14722  ruclem12  14970  dvdsle  15032  nndvdslegcd  15227  gcdnncl  15229  divgcdnn  15236  sqgcd  15278  eucalgf  15296  eucalginv  15297  lcmgcdlem  15319  lcmftp  15349  lcmfunsnlem2lem1  15351  lcmfunsnlem2lem2  15352  qredeu  15372  rpdvds  15374  cncongr2  15382  divnumden  15456  divdenle  15457  phisum  15495  oddprm  15515  pythagtriplem4  15524  pythagtriplem8  15528  pythagtriplem9  15529  pythagtriplem19  15538  4sqlem10  15651  ram0  15726  isipodrs  17161  gsumval2  17280  mulgnn  17547  sylow1lem1  18013  gsumval3eu  18305  abvtrivd  18840  00lss  18942  lvecvscan2  19112  fidomndrng  19307  mvrcl  19449  mplmon  19463  mplmonmul  19464  evlslem3  19514  coe1tmfv2  19645  cply1coe0  19669  cply1coe0bi  19670  prmirredlem  19841  uvcff  20130  1marepvsma1  20389  mdetrsca2  20410  mdetrlin2  20413  mdetunilem2  20419  mdetunilem5  20422  mdetunilem6  20423  mdetunilem9  20426  maducoeval2  20446  gsummatr01lem3  20463  gsummatr01lem4  20464  gsummatr01  20465  m2cpm  20546  m2cpminvid2lem  20559  fvmptnn04ifa  20655  fvmptnn04ifb  20656  fvmptnn04ifc  20657  chfacffsupp  20661  chfacfscmul0  20663  chfacfscmulgsum  20665  chfacfpmmul0  20667  chfacfpmmulgsum  20669  connclo  21218  dissnlocfin  21332  ptpjpre2  21383  txindis  21437  snfil  21668  alexsublem  21848  tsmsfbas  21931  stdbdxmet  22320  dscmet  22377  xrsxmet  22612  iccpnfcnv  22743  cphsubrglem  22977  minveclem3b  23199  minveclem4a  23201  ovolicc1  23284  dvexp2  23717  dvmptdiv  23737  lhop2  23778  deg1sublt  23870  ig1pval3  23934  dvply1  24039  plydiveu  24053  quotcan  24064  aaliou3lem9  24105  taylthlem2  24128  pserdvlem2  24182  abelthlem9  24194  logccne0  24325  logtayllem  24405  logtayl  24406  cxpef  24411  angrtmuld  24538  isosctrlem2  24549  isosctrlem3  24550  chordthmlem  24559  leibpilem2  24668  leibpi  24669  rlimcnp2  24693  efrlim  24696  vma1  24892  muinv  24919  lgsval2lem  25032  lgsval4  25042  lgsdir  25057  lgseisenlem4  25103  lgsquadlem1  25105  lgsquad2  25111  m1lgs  25113  2sqlem8a  25150  2sqlem8  25151  padicabv  25319  ostth1  25322  ostth3  25327  tgbtwnne  25385  tgbtwndiff  25401  tgcolg  25449  tgbtwnconn1lem3  25469  legso  25494  tglineeltr  25526  tglineintmo  25537  tglineneq  25539  colline  25544  mirne  25562  miriso  25565  mirhl  25574  mirbtwnhl  25575  symquadlem  25584  krippenlem  25585  midexlem  25587  ragncol  25604  footex  25613  colperp  25621  colperpexlem3  25624  mideulem2  25626  opphllem  25627  midex  25629  opptgdim2  25637  oppperpex  25645  hlpasch  25648  colopp  25661  colhp  25662  lmieu  25676  trgcopy  25696  cgracol  25719  cgrg3col4  25734  axlowdimlem15  25836  axcontlem2  25845  axcontlem7  25850  1egrvtxdg0  26407  2pthnloop  26627  cyclnspth  26695  eupth2lem1  27078  eupth2lem2  27079  eupth2lem3lem6  27093  strlem6  29115  hstrlem6  29123  atssma  29237  chirredlem1  29249  znsqcld  29512  xaddeq0  29518  xlt2addrd  29523  divnumden2  29564  2sqcoprm  29647  2sqmod  29648  submomnd  29710  ornglmullt  29807  orngrmullt  29808  ofldchr  29814  suborng  29815  pmtridf1o  29856  pmtridfv1  29857  pmtridfv2  29858  1smat1  29870  submatminr1  29876  madjusmdetlem2  29894  xrge0iifcnv  29979  xrge0iifcv  29980  xrge0iif1  29984  qqhval2lem  30025  qqhf  30030  qqhre  30064  esumrnmpt2  30130  esumcvgre  30153  inelpisys  30217  carsgclctunlem2  30381  ballotlemirc  30593  sgnmul  30604  sgn0bi  30609  signswlid  30636  repr0  30689  reprlt  30697  reprgt  30699  reprinfz1  30700  tgoldbachgtda  30739  tgoldbachgt  30741  bnj1523  31139  fz0n  31616  dfrdg2  31701  nolesgn2ores  31825  nosep1o  31832  nosepdmlem  31833  nosepssdm  31836  noresle  31846  nosupbnd1lem3  31856  nosupbnd1lem4  31857  nosupbnd1lem5  31858  nosupbnd1lem6  31859  nosupbnd2lem1  31861  dfrdg4  32058  broutsideof2  32229  outsidele  32239  rankeq1o  32278  ivthALT  32330  limsucncmpi  32444  topdifinffinlem  33195  icorempt2  33199  finxpreclem2  33227  finxp1o  33229  finxpreclem6  33233  poimirlem9  33418  poimirlem11  33420  poimirlem12  33421  poimirlem25  33434  fdc  33541  heibor1lem  33608  heiborlem4  33613  heiborlem6  33615  2atm  34813  lhpocnle  35302  lhp2at0nle  35321  trlval3  35474  cdleme18c  35580  cdlemg17b  35950  cdlemg17i  35957  dia2dimlem2  36354  dia2dimlem3  36355  dihord6apre  36545  dihatlat  36623  dochshpsat  36743  lcfrlem9  36839  mapdhval2  37015  hdmap1val2  37090  hdmap14lem4a  37163  hdmap14lem6  37165  jm2.26lem3  37568  kelac1  37633  clsk3nimkb  38338  clsk1indlem0  38339  sineq0ALT  39173  refsum2cnlem1  39196  disjxp1  39238  nelrnmpt  39257  disjf1  39369  disjrnmpt2  39375  disjinfi  39380  rnmptn0  39413  oddfl  39489  xrlttri5d  39495  supxrge  39554  nepnfltpnf  39558  nemnftgtmnft  39560  xrlexaddrp  39568  xrred  39581  supminfxr2  39699  icoiccdif  39750  qinioo  39762  ioonct  39764  fmul01lt1lem1  39816  climrec  39835  limcperiod  39860  reclimc  39885  limsupub  39936  cncfiooicclem1  40106  cncfioobdlem  40109  fperdvper  40133  dvdivbd  40138  ditgeqiooicc  40176  itgsincmulx  40190  itgioocnicc  40193  iblcncfioo  40194  stoweidlem35  40252  stoweidlem39  40256  stirlinglem5  40295  stirlinglem8  40298  dirkerper  40313  dirkercncflem2  40321  dirkercncflem4  40323  fourierdlem31  40355  fourierdlem34  40358  fourierdlem41  40365  fourierdlem42  40366  fourierdlem44  40368  fourierdlem48  40371  fourierdlem49  40372  fourierdlem53  40376  fourierdlem56  40379  fourierdlem58  40381  fourierdlem60  40383  fourierdlem61  40384  fourierdlem62  40385  fourierdlem65  40388  fourierdlem66  40389  fourierdlem73  40396  fourierdlem76  40399  fourierdlem79  40402  fourierdlem81  40404  fourierdlem82  40405  fourierdlem93  40416  fourierdlem103  40426  fourierdlem104  40427  sqwvfoura  40445  fourierswlem  40447  elaa2lem  40450  elaa2  40451  etransclem4  40455  etransclem24  40475  etransclem31  40482  etransclem32  40483  etransclem35  40486  sge0repnf  40603  sge0fodjrnlem  40633  sge0iunmpt  40635  sge0rpcpnf  40638  nnfoctbdjlem  40672  meadjun  40679  voliunsge0lem  40689  hoicvr  40762  ovnn0val  40765  ovnsubaddlem1  40784  hoidmvn0val  40798  hsphoidmvle  40800  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1lelem3  40807  ovnhoilem1  40815  ovnsubadd2lem  40859  ovnovollem3  40872  lighneallem3  41524  divgcdoddALTV  41593  dignn0flhalflem1  42409