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

Theorem neneqd 2568
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 2554 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylib 189 1  |-  ( ph  ->  -.  A  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1649    =/= wne 2552
This theorem is referenced by:  necon2bi  2598  necon2i  2599  pm2.21ddne  2626  nelrdva  3088  disjprg  4151  0inp0  4314  onnseq  6544  ackbij1lem15  8049  ttukeylem7  8330  fpwwe2lem13  8452  canthnumlem  8458  canthp1lem2  8463  recgt0  9788  elnnz  10226  xrnemnf  10652  xrnepnf  10653  fzprval  11039  expnnval  11314  elprchashprn2  11596  ruclem12  12769  dvdsle  12824  sqgcd  12987  eucalgf  13003  eucalginv  13004  qredeu  13036  divgcdodd  13048  rpdvds  13053  divnumden  13069  divdenle  13070  oddprm  13118  pythagtriplem4  13122  pythagtriplem8  13126  pythagtriplem9  13127  pythagtriplem19  13136  4sqlem10  13244  ram0  13319  isipodrs  14516  gsumval2  14712  mulgnn  14825  sylow1lem1  15161  gsumval3eu  15442  abvtrivd  15857  00lss  15947  lvecvscan2  16113  fidomndrng  16296  mvridlem  16412  mvrcl  16441  mplmon  16455  mplmonmul  16456  mplcoe3  16458  mplcoe2  16459  coe1tmfv2  16596  prmirredlem  16698  conclo  17401  ptpjpre2  17535  txindis  17589  snfil  17819  alexsublem  17998  tsmsfbas  18080  stdbdxmet  18437  dscmet  18493  xrsxmet  18713  iccpnfcnv  18842  cphsubrglem  19013  minveclem3b  19198  minveclem4a  19200  ovolicc1  19281  dvexp2  19709  lhop2  19768  evlslem3  19804  deg1sublt  19902  ig1pval3  19966  dvply1  20070  plydiveu  20084  quotcan  20095  aaliou3lem9  20136  taylthlem2  20159  pserdvlem2  20213  abelthlem9  20225  logtayllem  20419  logtayl  20420  cxpef  20425  angrtmuld  20519  isosctrlem2  20532  isosctrlem3  20533  chordthmlem  20542  leibpilem2  20650  leibpi  20651  rlimcnp2  20674  efrlim  20677  vma1  20818  muinv  20847  lgsval2lem  20959  lgsval4  20969  lgsdir  20983  lgseisenlem4  21005  lgsquadlem1  21007  lgsquad2  21013  m1lgs  21015  2sqlem8a  21024  2sqlem8  21025  padicabv  21193  ostth1  21196  ostth3  21201  isusgra0  21245  usgra1v  21277  cyclnspth  21468  eupath2lem1  21549  eupath2lem2  21550  eupath2lem3  21551  gxpval  21697  strlem6  23609  hstrlem6  23617  atssma  23731  chirredlem1  23743  xlt2addrd  23962  divnumden2  24001  xaddeq0  24032  ofldchr  24072  subofld  24073  xrge0iifcnv  24125  xrge0iifcv  24126  xrge0iif1  24130  qqhval2lem  24166  qqhf  24171  qqhre  24184  logccne0OLD  24193  logccne0  24194  ballotlemirc  24570  fz0n  24983  dfrdg2  25178  nobndup  25380  nobnddown  25381  dfrdg4  25515  axlowdimlem15  25611  axcontlem2  25620  axcontlem7  25625  broutsideof2  25772  outsidele  25782  rankeq1o  25828  limsucncmpi  25911  ivthALT  26031  fdc  26142  heibor1lem  26211  heiborlem4  26216  heiborlem6  26218  jm2.26lem3  26765  kelac1  26832  mamulid  27129  mamurid  27130  phisum  27189  refsum2cnlem1  27378  fmul01lt1lem1  27384  climrec  27399  stoweidlem35  27454  stoweidlem39  27458  stirlinglem5  27497  stirlinglem8  27500  frgra2v  27754  sgnp  27868  bnj1523  28780  2atm  29643  lhpocnle  30132  lhp2at0nle  30151  trlval3  30303  cdleme18c  30409  cdlemg17b  30778  cdlemg17i  30785  dia2dimlem2  31182  dia2dimlem3  31183  dihord6apre  31373  dihatlat  31451  dochshpsat  31571  lcfrlem9  31667  mapdhval2  31843  hdmap1val2  31918  hdmap14lem4a  31991  hdmap14lem6  31993
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-ne 2554
  Copyright terms: Public domain W3C validator