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

Theorem neneqd 2462
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 2448 . 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 1623    =/= wne 2446
This theorem is referenced by:  necon2bi  2492  necon2i  2493  pm2.21ddne  2520  disjprg  4019  0inp0  4182  onnseq  6361  ackbij1lem15  7860  ttukeylem7  8142  fpwwe2lem13  8264  canthnumlem  8270  canthp1lem2  8275  recgt0  9600  elnnz  10034  xrnemnf  10460  xrnepnf  10461  fzprval  10844  expnnval  11107  ruclem12  12519  dvdsle  12574  sqgcd  12737  eucalgf  12753  eucalginv  12754  qredeu  12786  divgcdodd  12798  rpdvds  12803  divnumden  12819  divdenle  12820  oddprm  12868  pythagtriplem4  12872  pythagtriplem8  12876  pythagtriplem9  12877  pythagtriplem19  12886  4sqlem10  12994  ram0  13069  isipodrs  14264  gsumval2  14460  mulgnn  14573  sylow1lem1  14909  gsumval3eu  15190  abvtrivd  15605  00lss  15699  lvecvscan2  15865  fidomndrng  16048  mvridlem  16164  mvrcl  16193  mplmon  16207  mplmonmul  16208  mplcoe3  16210  mplcoe2  16211  coe1tmfv2  16351  prmirredlem  16446  conclo  17141  ptpjpre2  17275  txindis  17328  snfil  17559  alexsublem  17738  tsmsfbas  17810  stdbdxmet  18061  dscmet  18095  xrsxmet  18315  iccpnfcnv  18442  cphsubrglem  18613  minveclem3b  18792  minveclem4a  18794  ovolicc1  18875  dvexp2  19303  lhop2  19362  evlslem3  19398  deg1sublt  19496  ig1pval3  19560  dvply1  19664  plydiveu  19678  quotcan  19689  aaliou3lem9  19730  taylthlem2  19753  pserdvlem2  19804  abelthlem9  19816  logtayllem  20006  logtayl  20007  cxpef  20012  angrtmuld  20106  isosctrlem2  20119  isosctrlem3  20120  chordthmlem  20129  leibpilem2  20237  leibpi  20238  rlimcnp2  20261  vma1  20404  muinv  20433  lgsval2lem  20545  lgsval4  20555  lgsdir  20569  lgseisenlem4  20591  lgsquadlem1  20593  lgsquad2  20599  m1lgs  20601  2sqlem8a  20610  2sqlem8  20611  padicabv  20779  ostth1  20782  ostth3  20787  gxpval  20926  strlem6  22836  hstrlem6  22844  atssma  22958  chirredlem1  22970  ballotlemirc  23090  xlt2addrd  23253  xaddeq0  23304  xrge0iifcnv  23315  xrge0iifcv  23316  xrge0iif1  23320  logccne0  23397  logccne0ALT  23398  pconcon  23762  eupath2lem1  23901  eupath2lem2  23902  eupath2lem3  23903  fz0n  24097  dfrdg2  24152  nobndup  24354  nobnddown  24355  dfrdg4  24488  axlowdimlem15  24584  axcontlem2  24593  axcontlem7  24598  broutsideof2  24745  outsidele  24755  limsucncmpi  24884  isconcl5a  26101  isconcl5ab  26102  ivthALT  26258  fdc  26455  heibor1lem  26533  heiborlem4  26538  heiborlem6  26540  jm2.26lem3  27094  kelac1  27161  mamulid  27458  mamurid  27459  phisum  27518  climrec  27729  stirlinglem5  27827  stirlinglem8  27830  elprchashprn2  28088  isusgra0  28106  usgra1v  28126  frgra2v  28177  sgnp  28247  bnj1523  29101  2atm  29716  lhpocnle  30205  lhp2at0nle  30224  trlval3  30376  cdleme18c  30482  cdlemg17b  30851  cdlemg17i  30858  dia2dimlem2  31255  dia2dimlem3  31256  dihord6apre  31446  dihatlat  31524  dochshpsat  31644  lcfrlem9  31740  mapdhval2  31916  hdmap1val2  31991  hdmap14lem4a  32064  hdmap14lem6  32066
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 2448
  Copyright terms: Public domain W3C validator