MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neneqd Structured version   Unicode version

Theorem neneqd 2621
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
StepHypRef Expression
1 neneqd.1 . 2  |-  ( ph  ->  A  =/=  B )
2 df-ne 2616 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylib 199 1  |-  ( ph  ->  -.  A  =  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1437    =/= wne 2614
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 188  df-ne 2616
This theorem is referenced by:  neneq  2622  necon3ad  2630  necon2bi  2657  necon2i  2663  necon4i  2664  pm2.21ddne  2734  nelrdva  3281  disjprg  4419  0inp0  4596  onnseq  7074  sniffsupp  7932  ackbij1lem15  8671  ttukeylem7  8952  fpwwe2lem13  9074  canthnumlem  9080  canthp1lem2  9085  recgt0  10456  elnnz  10954  xrnemnf  11426  xrnepnf  11427  fzprval  11863  expnnval  12281  elprchashprn2  12579  relexpsucnnr  13088  relexp1g  13089  relexpuzrel  13115  sgnp  13153  fprodn0f  14044  ruclem12  14292  dvdsle  14349  nndvdslegcd  14478  gcdnncl  14480  sqgcd  14525  eucalgf  14541  eucalginv  14542  lcmgcdlem  14570  lcmftp  14608  lcmfunsnlem2lem1  14610  lcmfunsnlem2lem2  14611  divgcdodd  14652  qredeu  14663  rpdvds  14675  divnumden  14696  divdenle  14697  oddprm  14764  pythagtriplem4  14768  pythagtriplem8  14772  pythagtriplem9  14773  pythagtriplem19  14782  4sqlem10  14890  ram0  14979  isipodrs  16406  gsumval2  16522  mulgnn  16763  sylow1lem1  17249  gsumval3eu  17537  abvtrivd  18067  00lss  18164  lvecvscan2  18334  fidomndrng  18530  mvrcl  18672  mplmon  18686  mplmonmul  18687  evlslem3  18736  coe1tmfv2  18867  cply1coe0  18892  cply1coe0bi  18893  prmirredlem  19062  uvcff  19347  1marepvsma1  19606  mdetrsca2  19627  mdetrlin2  19630  mdetunilem2  19636  mdetunilem5  19639  mdetunilem6  19640  mdetunilem9  19643  maducoeval2  19663  gsummatr01lem3  19680  gsummatr01lem4  19681  gsummatr01  19682  m2cpm  19763  m2cpminvid2lem  19776  fvmptnn04ifa  19872  fvmptnn04ifb  19873  fvmptnn04ifc  19874  chfacffsupp  19878  chfacfscmul0  19880  chfacfscmulgsum  19882  chfacfpmmul0  19884  chfacfpmmulgsum  19886  conclo  20428  dissnlocfin  20542  ptpjpre2  20593  txindis  20647  snfil  20877  alexsublem  21057  tsmsfbas  21140  stdbdxmet  21528  dscmet  21585  xrsxmet  21825  iccpnfcnv  21970  cphsubrglem  22153  minveclem3b  22368  minveclem4a  22370  minveclem3bOLD  22380  minveclem4aOLD  22382  ovolicc1  22467  dvexp2  22906  lhop2  22965  deg1sublt  23057  ig1pval3  23124  ig1pval3OLD  23130  dvply1  23235  plydiveu  23249  quotcan  23260  aaliou3lem9  23304  taylthlem2  23327  pserdvlem2  23381  abelthlem9  23393  logccne0  23526  logtayllem  23602  logtayl  23603  cxpef  23608  angrtmuld  23735  isosctrlem2  23746  isosctrlem3  23747  chordthmlem  23756  leibpilem2  23865  leibpi  23866  rlimcnp2  23890  efrlim  23893  vma1  24091  muinv  24120  lgsval2lem  24232  lgsval4  24242  lgsdir  24256  lgseisenlem4  24278  lgsquadlem1  24280  lgsquad2  24286  m1lgs  24288  2sqlem8a  24297  2sqlem8  24298  padicabv  24466  ostth1  24469  ostth3  24474  tgbtwnne  24532  tgbtwndiff  24548  tgcolg  24597  tgbtwnconn1lem3  24617  legso  24642  tglineeltr  24674  tglineintmo  24685  tglineneq  24687  colline  24692  mirne  24710  miriso  24713  mirhl  24722  mirbtwnhl  24723  symquadlem  24732  krippenlem  24733  midexlem  24735  ragncol  24752  footex  24761  colperp  24769  colperpexlem3  24772  mideulem2  24774  opphllem  24775  midex  24777  opptgdim2  24785  oppperpex  24793  hlpasch  24796  colopp  24809  colhp  24810  lmieu  24824  trgcopy  24844  cgracol  24867  cgrg3col4  24882  axlowdimlem15  24984  axcontlem2  24993  axcontlem7  24998  isusgra0  25072  usgraop  25075  usgra1v  25115  cyclnspth  25357  clwwlkn0  25500  rusgra0edg  25681  eupath2lem1  25703  eupath2lem2  25704  eupath2lem3  25705  gxpval  25985  strlem6  27907  hstrlem6  27915  atssma  28029  chirredlem1  28041  znsqcld  28329  xaddeq0  28336  xlt2addrd  28344  divnumden2  28388  2sqcoprm  28415  2sqmod  28416  submomnd  28480  ornglmullt  28578  orngrmullt  28579  ofldchr  28585  suborng  28586  1smat1  28638  submatminr1  28644  madjusmdetlem2  28662  xrge0iifcnv  28747  xrge0iifcv  28748  xrge0iif1  28752  qqhval2lem  28793  qqhf  28798  qqhre  28832  esumrnmpt2  28897  esumcvgre  28920  inelpisys  28984  carsgclctunlem2  29159  ballotlemirc  29372  ballotlemircOLD  29410  sgnmul  29421  sgn0bi  29426  signswlid  29456  bnj1523  29888  fz0n  30371  dfrdg2  30449  nobndup  30594  nobnddown  30595  dfrdg4  30723  broutsideof2  30894  outsidele  30904  rankeq1o  30943  ivthALT  30996  limsucncmpi  31110  topdifinffinlem  31714  icorempt2  31718  finxpreclem2  31746  finxp1o  31748  finxpreclem6  31752  poimirlem9  31913  poimirlem11  31915  poimirlem12  31916  poimirlem25  31929  fdc  32038  heibor1lem  32105  heiborlem4  32110  heiborlem6  32112  2atm  33061  lhpocnle  33550  lhp2at0nle  33569  trlval3  33722  cdleme18c  33828  cdlemg17b  34198  cdlemg17i  34205  dia2dimlem2  34602  dia2dimlem3  34603  dihord6apre  34793  dihatlat  34871  dochshpsat  34991  lcfrlem9  35087  mapdhval2  35263  hdmap1val2  35338  hdmap14lem4a  35411  hdmap14lem6  35413  jm2.26lem3  35826  kelac1  35891  phisum  36046  sineq0ALT  37307  refsum2cnlem1  37331  disjxp1  37384  disjf1  37418  disjrnmpt2  37424  disjinfi  37429  oddfl  37441  xrlttri5d  37447  supxrge  37515  nepnfltpnf  37519  nemnftgtmnft  37521  xrlexaddrp  37529  icoiccdif  37574  fmul01lt1lem1  37602  climrec  37621  limcperiod  37648  reclimc  37674  cncfiooicclem1  37711  cncfioobdlem  37714  dvmptdiv  37729  fperdvper  37730  dvdivbd  37735  ditgeqiooicc  37777  itgsincmulx  37791  itgioocnicc  37794  iblcncfioo  37795  stoweidlem35  37836  stoweidlem39  37840  stirlinglem5  37880  stirlinglem8  37883  dirkerper  37898  dirkercncflem2  37906  dirkercncflem4  37908  fourierdlem31  37940  fourierdlem31OLD  37941  fourierdlem34  37944  fourierdlem41  37951  fourierdlem42  37952  fourierdlem42OLD  37953  fourierdlem44  37955  fourierdlem48  37958  fourierdlem49  37959  fourierdlem53  37963  fourierdlem56  37966  fourierdlem58  37968  fourierdlem60  37970  fourierdlem61  37971  fourierdlem62  37972  fourierdlem65  37975  fourierdlem66  37976  fourierdlem73  37983  fourierdlem76  37986  fourierdlem79  37989  fourierdlem81  37991  fourierdlem82  37992  fourierdlem93  38003  fourierdlem103  38013  fourierdlem104  38014  sqwvfoura  38032  fourierswlem  38034  elaa2lem  38037  elaa2lemOLD  38038  elaa2  38039  etransclem4  38043  etransclem24  38063  etransclem31  38070  etransclem32  38071  etransclem35  38074  sge0repnf  38136  sge0fodjrnlem  38166  sge0iunmpt  38168  sge0rpcpnf  38171  nnfoctbdjlem  38201  meadjun  38208  hoicvr  38274  ovnn0val  38277  ovnsubaddlem1  38296  hoidmvn0val  38310  hsphoidmvle  38312  hoidmv1lelem1  38317  hoidmv1lelem2  38318  hoidmv1lelem3  38319  ovnhoilem1  38327  divgcdoddALTV  38681  isusgr0  39036  ausgrumgri  39048  usgr1vr  39105  dignn0flhalflem1  40047
  Copyright terms: Public domain W3C validator