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

Theorem neneqd 2583
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 2569 . 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 2567
This theorem is referenced by:  necon2bi  2613  necon2i  2614  pm2.21ddne  2641  nelrdva  3103  disjprg  4168  0inp0  4331  onnseq  6565  ackbij1lem15  8070  ttukeylem7  8351  fpwwe2lem13  8473  canthnumlem  8479  canthp1lem2  8484  recgt0  9810  elnnz  10248  xrnemnf  10674  xrnepnf  10675  fzprval  11062  expnnval  11340  elprchashprn2  11622  ruclem12  12795  dvdsle  12850  sqgcd  13013  eucalgf  13029  eucalginv  13030  qredeu  13062  divgcdodd  13074  rpdvds  13079  divnumden  13095  divdenle  13096  oddprm  13144  pythagtriplem4  13148  pythagtriplem8  13152  pythagtriplem9  13153  pythagtriplem19  13162  4sqlem10  13270  ram0  13345  isipodrs  14542  gsumval2  14738  mulgnn  14851  sylow1lem1  15187  gsumval3eu  15468  abvtrivd  15883  00lss  15973  lvecvscan2  16139  fidomndrng  16322  mvridlem  16438  mvrcl  16467  mplmon  16481  mplmonmul  16482  mplcoe3  16484  mplcoe2  16485  coe1tmfv2  16622  prmirredlem  16728  conclo  17431  ptpjpre2  17565  txindis  17619  snfil  17849  alexsublem  18028  tsmsfbas  18110  stdbdxmet  18498  dscmet  18573  xrsxmet  18793  iccpnfcnv  18922  cphsubrglem  19093  minveclem3b  19282  minveclem4a  19284  ovolicc1  19365  dvexp2  19793  lhop2  19852  evlslem3  19888  deg1sublt  19986  ig1pval3  20050  dvply1  20154  plydiveu  20168  quotcan  20179  aaliou3lem9  20220  taylthlem2  20243  pserdvlem2  20297  abelthlem9  20309  logtayllem  20503  logtayl  20504  cxpef  20509  angrtmuld  20603  isosctrlem2  20616  isosctrlem3  20617  chordthmlem  20626  leibpilem2  20734  leibpi  20735  rlimcnp2  20758  efrlim  20761  vma1  20902  muinv  20931  lgsval2lem  21043  lgsval4  21053  lgsdir  21067  lgseisenlem4  21089  lgsquadlem1  21091  lgsquad2  21097  m1lgs  21099  2sqlem8a  21108  2sqlem8  21109  padicabv  21277  ostth1  21280  ostth3  21285  isusgra0  21329  usgra1v  21362  cyclnspth  21571  eupath2lem1  21652  eupath2lem2  21653  eupath2lem3  21654  gxpval  21800  strlem6  23712  hstrlem6  23720  atssma  23834  chirredlem1  23846  xaddeq0  24072  xlt2addrd  24077  divnumden2  24114  ofldchr  24197  subofld  24198  xrge0iifcnv  24272  xrge0iifcv  24273  xrge0iif1  24277  qqhval2lem  24318  qqhf  24323  qqhre  24339  logccne0OLD  24348  logccne0  24349  ballotlemirc  24742  fz0n  25155  dfrdg2  25366  nobndup  25568  nobnddown  25569  dfrdg4  25703  axlowdimlem15  25799  axcontlem2  25808  axcontlem7  25813  broutsideof2  25960  outsidele  25970  rankeq1o  26016  limsucncmpi  26099  ivthALT  26228  fdc  26339  heibor1lem  26408  heiborlem4  26413  heiborlem6  26415  jm2.26lem3  26962  kelac1  27029  mamulid  27326  mamurid  27327  phisum  27386  refsum2cnlem1  27575  fmul01lt1lem1  27581  climrec  27596  stoweidlem35  27651  stoweidlem39  27655  stirlinglem5  27694  stirlinglem8  27697  frgra2v  28103  sgnp  28234  bnj1523  29146  2atm  30009  lhpocnle  30498  lhp2at0nle  30517  trlval3  30669  cdleme18c  30775  cdlemg17b  31144  cdlemg17i  31151  dia2dimlem2  31548  dia2dimlem3  31549  dihord6apre  31739  dihatlat  31817  dochshpsat  31937  lcfrlem9  32033  mapdhval2  32209  hdmap1val2  32284  hdmap14lem4a  32357  hdmap14lem6  32359
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 2569
  Copyright terms: Public domain W3C validator