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

Theorem neneqd 2614
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 2598 . 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 1362    =/= wne 2596
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 2598
This theorem is referenced by:  necon2bi  2647  necon2i  2648  pm2.21ddne  2675  nelrdva  3157  disjprg  4276  0inp0  4452  onnseq  6791  sniffsupp  7647  ackbij1lem15  8391  ttukeylem7  8672  fpwwe2lem13  8796  canthnumlem  8802  canthp1lem2  8807  recgt0  10160  elnnz  10643  xrnemnf  11086  xrnepnf  11087  fzprval  11500  expnnval  11851  elprchashprn2  12139  sgnp  12562  ruclem12  13505  dvdsle  13560  sqgcd  13724  eucalgf  13740  eucalginv  13741  qredeu  13775  divgcdodd  13787  rpdvds  13792  divnumden  13808  divdenle  13809  oddprm  13864  pythagtriplem4  13868  pythagtriplem8  13872  pythagtriplem9  13873  pythagtriplem19  13882  4sqlem10  13990  ram0  14065  isipodrs  15313  gsumval2  15492  mulgnn  15612  sylow1lem1  16076  gsumval3eu  16360  abvtrivd  16848  00lss  16944  lvecvscan2  17114  fidomndrng  17300  mvridlemOLD  17425  mvrcl  17461  mplmon  17475  mplmonmul  17476  mplcoe3OLD  17479  mplcoe2OLD  17481  coe1tmfv2  17625  prmirredlem  17758  prmirredlemOLD  17761  uvcff  18057  1marepvsma1  18235  mdet1  18249  mdetrsca2  18252  mdetrlin2  18254  mdetunilem2  18260  mdetunilem6  18264  mdetunilem9  18267  maducoeval2  18287  gsummatr01lem3  18304  gsummatr01lem4  18305  gsummatr01  18306  conclo  18860  ptpjpre2  18994  txindis  19048  snfil  19278  alexsublem  19457  tsmsfbas  19539  stdbdxmet  19931  dscmet  20006  xrsxmet  20227  iccpnfcnv  20357  cphsubrglem  20537  minveclem3b  20756  minveclem4a  20758  ovolicc1  20840  dvexp2  21269  lhop2  21328  evlslem3  21365  deg1sublt  21466  ig1pval3  21530  dvply1  21634  plydiveu  21648  quotcan  21659  aaliou3lem9  21700  taylthlem2  21723  pserdvlem2  21777  abelthlem9  21789  logtayllem  21988  logtayl  21989  cxpef  21994  angrtmuld  22088  isosctrlem2  22101  isosctrlem3  22102  chordthmlem  22111  leibpilem2  22220  leibpi  22221  rlimcnp2  22244  efrlim  22247  vma1  22388  muinv  22417  lgsval2lem  22529  lgsval4  22539  lgsdir  22553  lgseisenlem4  22575  lgsquadlem1  22577  lgsquad2  22583  m1lgs  22585  2sqlem8a  22594  2sqlem8  22595  padicabv  22763  ostth1  22766  ostth3  22771  tgbtwndiff  22840  tgcolg  22866  tgbtwnconn1lem3  22881  tglineeltr  22907  tglineintmo  22916  colline  22917  miriso  22934  axlowdimlem15  23024  axcontlem2  23033  axcontlem7  23038  isusgra0  23097  usgra1v  23130  cyclnspth  23339  eupath2lem1  23420  eupath2lem2  23421  eupath2lem3  23422  gxpval  23568  strlem6  25482  hstrlem6  25490  atssma  25604  chirredlem1  25616  xaddeq0  25870  xlt2addrd  25875  divnumden2  25909  submomnd  25996  ornglmullt  26127  orngrmullt  26128  ofldchr  26134  suborng  26135  xrge0iifcnv  26216  xrge0iifcv  26217  xrge0iif1  26221  qqhval2lem  26263  qqhf  26268  qqhre  26299  logccne0OLD  26307  logccne0  26308  ballotlemirc  26761  sgnmul  26772  sgnsub  26774  sgn0bi  26777  sgnmulsgn  26779  sgnmulsgp  26780  signswlid  26807  fz0n  27235  dfrdg2  27455  nobndup  27687  nobnddown  27688  dfrdg4  27827  broutsideof2  27999  outsidele  28009  rankeq1o  28055  limsucncmpi  28138  ivthALT  28371  fdc  28482  heibor1lem  28549  heiborlem4  28554  heiborlem6  28556  jm2.26lem3  29192  kelac1  29258  phisum  29409  refsum2cnlem1  29601  fmul01lt1lem1  29607  climrec  29619  stoweidlem35  29673  stoweidlem39  29677  stirlinglem5  29716  stirlinglem8  29719  clwwlkn0  30280  rusgra0edg  30416  sineq0ALT  31372  bnj1523  31761  2atm  32741  lhpocnle  33230  lhp2at0nle  33249  trlval3  33401  cdleme18c  33507  cdlemg17b  33876  cdlemg17i  33883  dia2dimlem2  34280  dia2dimlem3  34281  dihord6apre  34471  dihatlat  34549  dochshpsat  34669  lcfrlem9  34765  mapdhval2  34941  hdmap1val2  35016  hdmap14lem4a  35089  hdmap14lem6  35091
  Copyright terms: Public domain W3C validator