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 2600 . 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 1652    =/= wne 2598
This theorem is referenced by:  necon2bi  2644  necon2i  2645  pm2.21ddne  2672  nelrdva  3135  disjprg  4200  0inp0  4363  onnseq  6598  ackbij1lem15  8104  ttukeylem7  8385  fpwwe2lem13  8507  canthnumlem  8513  canthp1lem2  8518  recgt0  9844  elnnz  10282  xrnemnf  10708  xrnepnf  10709  fzprval  11096  expnnval  11375  elprchashprn2  11657  ruclem12  12830  dvdsle  12885  sqgcd  13048  eucalgf  13064  eucalginv  13065  qredeu  13097  divgcdodd  13109  rpdvds  13114  divnumden  13130  divdenle  13131  oddprm  13179  pythagtriplem4  13183  pythagtriplem8  13187  pythagtriplem9  13188  pythagtriplem19  13197  4sqlem10  13305  ram0  13380  isipodrs  14577  gsumval2  14773  mulgnn  14886  sylow1lem1  15222  gsumval3eu  15503  abvtrivd  15918  00lss  16008  lvecvscan2  16174  fidomndrng  16357  mvridlem  16473  mvrcl  16502  mplmon  16516  mplmonmul  16517  mplcoe3  16519  mplcoe2  16520  coe1tmfv2  16657  prmirredlem  16763  conclo  17468  ptpjpre2  17602  txindis  17656  snfil  17886  alexsublem  18065  tsmsfbas  18147  stdbdxmet  18535  dscmet  18610  xrsxmet  18830  iccpnfcnv  18959  cphsubrglem  19130  minveclem3b  19319  minveclem4a  19321  ovolicc1  19402  dvexp2  19830  lhop2  19889  evlslem3  19925  deg1sublt  20023  ig1pval3  20087  dvply1  20191  plydiveu  20205  quotcan  20216  aaliou3lem9  20257  taylthlem2  20280  pserdvlem2  20334  abelthlem9  20346  logtayllem  20540  logtayl  20541  cxpef  20546  angrtmuld  20640  isosctrlem2  20653  isosctrlem3  20654  chordthmlem  20663  leibpilem2  20771  leibpi  20772  rlimcnp2  20795  efrlim  20798  vma1  20939  muinv  20968  lgsval2lem  21080  lgsval4  21090  lgsdir  21104  lgseisenlem4  21126  lgsquadlem1  21128  lgsquad2  21134  m1lgs  21136  2sqlem8a  21145  2sqlem8  21146  padicabv  21314  ostth1  21317  ostth3  21322  isusgra0  21366  usgra1v  21399  cyclnspth  21608  eupath2lem1  21689  eupath2lem2  21690  eupath2lem3  21691  gxpval  21837  strlem6  23749  hstrlem6  23757  atssma  23871  chirredlem1  23883  xaddeq0  24109  xlt2addrd  24114  divnumden2  24151  ofldchr  24234  subofld  24235  xrge0iifcnv  24309  xrge0iifcv  24310  xrge0iif1  24314  qqhval2lem  24355  qqhf  24360  qqhre  24376  logccne0OLD  24385  logccne0  24386  ballotlemirc  24779  fz0n  25192  dfrdg2  25411  nobndup  25620  nobnddown  25621  dfrdg4  25760  axlowdimlem15  25860  axcontlem2  25869  axcontlem7  25874  broutsideof2  26021  outsidele  26031  rankeq1o  26077  limsucncmpi  26160  ivthALT  26292  fdc  26403  heibor1lem  26472  heiborlem4  26477  heiborlem6  26479  jm2.26lem3  27026  kelac1  27093  mamulid  27390  mamurid  27391  phisum  27450  refsum2cnlem1  27639  fmul01lt1lem1  27645  climrec  27660  stoweidlem35  27715  stoweidlem39  27719  stirlinglem5  27758  stirlinglem8  27761  frgra2v  28290  sgnp  28421  sineq0ALT  28950  bnj1523  29341  2atm  30225  lhpocnle  30714  lhp2at0nle  30733  trlval3  30885  cdleme18c  30991  cdlemg17b  31360  cdlemg17i  31367  dia2dimlem2  31764  dia2dimlem3  31765  dihord6apre  31955  dihatlat  32033  dochshpsat  32153  lcfrlem9  32249  mapdhval2  32425  hdmap1val2  32500  hdmap14lem4a  32573  hdmap14lem6  32575
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 2600
  Copyright terms: Public domain W3C validator