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

Theorem neneqd 2669
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 2664 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylib 196 1  |-  ( ph  ->  -.  A  =  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1379    =/= wne 2662
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 185  df-ne 2664
This theorem is referenced by:  necon3ad  2677  necon2bi  2704  necon2i  2710  necon4i  2711  pm2.21ddne  2781  nelrdva  3313  disjprg  4443  0inp0  4619  onnseq  7015  sniffsupp  7869  ackbij1lem15  8614  ttukeylem7  8895  fpwwe2lem13  9020  canthnumlem  9026  canthp1lem2  9031  recgt0  10386  elnnz  10874  xrnemnf  11328  xrnepnf  11329  fzprval  11740  expnnval  12137  elprchashprn2  12429  sgnp  12886  ruclem12  13835  dvdsle  13890  sqgcd  14055  eucalgf  14071  eucalginv  14072  qredeu  14107  divgcdodd  14119  rpdvds  14124  divnumden  14140  divdenle  14141  oddprm  14198  pythagtriplem4  14202  pythagtriplem8  14206  pythagtriplem9  14207  pythagtriplem19  14216  4sqlem10  14324  ram0  14399  isipodrs  15648  gsumval2  15835  mulgnn  15958  sylow1lem1  16424  gsumval3eu  16710  abvtrivd  17289  00lss  17388  lvecvscan2  17558  fidomndrng  17755  mvridlemOLD  17874  mvrcl  17910  mplmon  17924  mplmonmul  17925  mplcoe3OLD  17928  mplcoe2OLD  17932  evlslem3  17982  coe1tmfv2  18115  cply1coe0  18140  cply1coe0bi  18141  prmirredlem  18318  prmirredlemOLD  18321  uvcff  18617  1marepvsma1  18880  mdetrsca2  18901  mdetrlin2  18904  mdetunilem2  18910  mdetunilem6  18914  mdetunilem9  18917  maducoeval2  18937  gsummatr01lem3  18954  gsummatr01lem4  18955  gsummatr01  18956  m2cpm  19037  m2cpminvid2lem  19050  fvmptnn04ifa  19146  fvmptnn04ifb  19147  fvmptnn04ifc  19148  chfacffsupp  19152  chfacfscmul0  19154  chfacfscmulgsum  19156  chfacfpmmul0  19158  chfacfpmmulgsum  19160  conclo  19710  ptpjpre2  19844  txindis  19898  snfil  20128  alexsublem  20307  tsmsfbas  20389  stdbdxmet  20781  dscmet  20856  xrsxmet  21077  iccpnfcnv  21207  cphsubrglem  21387  minveclem3b  21606  minveclem4a  21608  ovolicc1  21690  dvexp2  22120  lhop2  22179  deg1sublt  22274  ig1pval3  22338  dvply1  22442  plydiveu  22456  quotcan  22467  aaliou3lem9  22508  taylthlem2  22531  pserdvlem2  22585  abelthlem9  22597  logtayllem  22796  logtayl  22797  cxpef  22802  angrtmuld  22896  isosctrlem2  22909  isosctrlem3  22910  chordthmlem  22919  leibpilem2  23028  leibpi  23029  rlimcnp2  23052  efrlim  23055  vma1  23196  muinv  23225  lgsval2lem  23337  lgsval4  23347  lgsdir  23361  lgseisenlem4  23383  lgsquadlem1  23385  lgsquad2  23391  m1lgs  23393  2sqlem8a  23402  2sqlem8  23403  padicabv  23571  ostth1  23574  ostth3  23579  tgbtwnne  23637  tgbtwndiff  23653  tgcolg  23697  tgbtwnconn1lem3  23716  legso  23740  tglineeltr  23753  tglineintmo  23763  tglineneq  23765  coltr2  23769  colline  23771  miriso  23791  symquadlem  23802  krippenlem  23803  midexlem  23805  ragncol  23822  footex  23831  colperp  23836  colperpexlem3  23839  mideulem  23841  mideu  23842  lmieu  23855  axlowdimlem15  23963  axcontlem2  23972  axcontlem7  23977  isusgra0  24051  usgraop  24054  usgra1v  24094  cyclnspth  24335  clwwlkn0  24478  rusgra0edg  24659  eupath2lem1  24681  eupath2lem2  24682  eupath2lem3  24683  gxpval  24965  strlem6  26879  hstrlem6  26887  atssma  27001  chirredlem1  27013  xaddeq0  27269  xlt2addrd  27274  divnumden2  27304  submomnd  27390  ornglmullt  27488  orngrmullt  27489  ofldchr  27495  suborng  27496  xrge0iifcnv  27579  xrge0iifcv  27580  xrge0iif1  27584  qqhval2lem  27626  qqhf  27631  qqhre  27662  logccne0OLD  27679  logccne0  27680  ballotlemirc  28138  sgnmul  28149  sgnsub  28151  sgn0bi  28154  sgnmulsgn  28156  sgnmulsgp  28157  signswlid  28184  fz0n  28613  dfrdg2  28833  nobndup  29065  nobnddown  29066  dfrdg4  29205  broutsideof2  29377  outsidele  29387  rankeq1o  29433  limsucncmpi  29515  ivthALT  29758  fdc  29869  heibor1lem  29936  heiborlem4  29941  heiborlem6  29943  jm2.26lem3  30575  kelac1  30641  phisum  30792  lcmgcdlem  30840  refsum2cnlem1  31018  neneq  31039  oddfl  31064  xrlttri5d  31070  icoiccdif  31156  fmul01lt1lem1  31162  climrec  31173  limcperiod  31198  reclimc  31223  cncfiooicclem1  31260  cncfioobdlem  31263  dvmptdiv  31275  fperdvper  31276  dvdivbd  31281  ditgeqiooicc  31306  itgsincmulx  31320  itgioocnicc  31323  stoweidlem35  31363  stoweidlem39  31367  stirlinglem5  31406  stirlinglem8  31409  dirkerper  31424  dirkercncflem2  31432  dirkercncflem4  31434  fourierdlem31  31466  fourierdlem34  31469  fourierdlem41  31476  fourierdlem42  31477  fourierdlem44  31479  fourierdlem48  31483  fourierdlem49  31484  fourierdlem53  31488  fourierdlem56  31491  fourierdlem58  31493  fourierdlem60  31495  fourierdlem61  31496  fourierdlem62  31497  fourierdlem65  31500  fourierdlem66  31501  fourierdlem73  31508  fourierdlem74  31509  fourierdlem75  31510  fourierdlem76  31511  fourierdlem79  31514  fourierdlem81  31516  fourierdlem82  31517  fourierdlem93  31528  fourierdlem103  31538  fourierdlem104  31539  sqwvfoura  31557  fourierswlem  31559  sineq0ALT  32835  bnj1523  33224  2atm  34341  lhpocnle  34830  lhp2at0nle  34849  trlval3  35001  cdleme18c  35107  cdlemg17b  35476  cdlemg17i  35483  dia2dimlem2  35880  dia2dimlem3  35881  dihord6apre  36071  dihatlat  36149  dochshpsat  36269  lcfrlem9  36365  mapdhval2  36541  hdmap1val2  36616  hdmap14lem4a  36689  hdmap14lem6  36691
  Copyright terms: Public domain W3C validator