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

Theorem neneqd 2475
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 2461 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylib 188 1  |-  ( ph  ->  -.  A  =  B )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  necon2bi  2505  necon2i  2506  pm2.21ddne  2533  disjprg  4035  0inp0  4198  onnseq  6377  ackbij1lem15  7876  ttukeylem7  8158  fpwwe2lem13  8280  canthnumlem  8286  canthp1lem2  8291  recgt0  9616  elnnz  10050  xrnemnf  10476  xrnepnf  10477  fzprval  10860  expnnval  11123  ruclem12  12535  dvdsle  12590  sqgcd  12753  eucalgf  12769  eucalginv  12770  qredeu  12802  divgcdodd  12814  rpdvds  12819  divnumden  12835  divdenle  12836  oddprm  12884  pythagtriplem4  12888  pythagtriplem8  12892  pythagtriplem9  12893  pythagtriplem19  12902  4sqlem10  13010  ram0  13085  isipodrs  14280  gsumval2  14476  mulgnn  14589  sylow1lem1  14925  gsumval3eu  15206  abvtrivd  15621  00lss  15715  lvecvscan2  15881  fidomndrng  16064  mvridlem  16180  mvrcl  16209  mplmon  16223  mplmonmul  16224  mplcoe3  16226  mplcoe2  16227  coe1tmfv2  16367  prmirredlem  16462  conclo  17157  ptpjpre2  17291  txindis  17344  snfil  17575  alexsublem  17754  tsmsfbas  17826  stdbdxmet  18077  dscmet  18111  xrsxmet  18331  iccpnfcnv  18458  cphsubrglem  18629  minveclem3b  18808  minveclem4a  18810  ovolicc1  18891  dvexp2  19319  lhop2  19378  evlslem3  19414  deg1sublt  19512  ig1pval3  19576  dvply1  19680  plydiveu  19694  quotcan  19705  aaliou3lem9  19746  taylthlem2  19769  pserdvlem2  19820  abelthlem9  19832  logtayllem  20022  logtayl  20023  cxpef  20028  angrtmuld  20122  isosctrlem2  20135  isosctrlem3  20136  chordthmlem  20145  leibpilem2  20253  leibpi  20254  rlimcnp2  20277  vma1  20420  muinv  20449  lgsval2lem  20561  lgsval4  20571  lgsdir  20585  lgseisenlem4  20607  lgsquadlem1  20609  lgsquad2  20615  m1lgs  20617  2sqlem8a  20626  2sqlem8  20627  padicabv  20795  ostth1  20798  ostth3  20803  gxpval  20942  strlem6  22852  hstrlem6  22860  atssma  22974  chirredlem1  22986  ballotlemirc  23106  xlt2addrd  23268  xaddeq0  23319  xrge0iifcnv  23330  xrge0iifcv  23331  xrge0iif1  23335  logccne0  23412  logccne0ALT  23413  pconcon  23777  eupath2lem1  23916  eupath2lem2  23917  eupath2lem3  23918  fz0n  24112  dfrdg2  24223  nobndup  24425  nobnddown  24426  dfrdg4  24560  axlowdimlem15  24656  axcontlem2  24665  axcontlem7  24670  broutsideof2  24817  outsidele  24827  limsucncmpi  24956  isconcl5a  26204  isconcl5ab  26205  ivthALT  26361  fdc  26558  heibor1lem  26636  heiborlem4  26641  heiborlem6  26643  jm2.26lem3  27197  kelac1  27264  mamulid  27561  mamurid  27562  phisum  27621  climrec  27832  stirlinglem5  27930  stirlinglem8  27933  elprchashprn2  28216  isusgra0  28238  usgra1v  28260  cyclnspth  28376  frgra2v  28423  sgnp  28501  bnj1523  29417  2atm  30338  lhpocnle  30827  lhp2at0nle  30846  trlval3  30998  cdleme18c  31104  cdlemg17b  31473  cdlemg17i  31480  dia2dimlem2  31877  dia2dimlem3  31878  dihord6apre  32068  dihatlat  32146  dochshpsat  32266  lcfrlem9  32362  mapdhval2  32538  hdmap1val2  32613  hdmap14lem4a  32686  hdmap14lem6  32688
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 177  df-ne 2461
  Copyright terms: Public domain W3C validator