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

Theorem neneqd 2645
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 2640 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylib 196 1  |-  ( ph  ->  -.  A  =  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1383    =/= wne 2638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-ne 2640
This theorem is referenced by:  necon3ad  2653  necon2bi  2680  necon2i  2686  necon4i  2687  pm2.21ddne  2757  nelrdva  3295  disjprg  4433  0inp0  4609  onnseq  7017  sniffsupp  7871  ackbij1lem15  8617  ttukeylem7  8898  fpwwe2lem13  9023  canthnumlem  9029  canthp1lem2  9034  recgt0  10393  elnnz  10881  xrnemnf  11338  xrnepnf  11339  fzprval  11750  expnnval  12150  elprchashprn2  12442  sgnp  12904  ruclem12  13955  dvdsle  14012  sqgcd  14177  eucalgf  14193  eucalginv  14194  qredeu  14229  divgcdodd  14241  rpdvds  14246  divnumden  14262  divdenle  14263  oddprm  14320  pythagtriplem4  14324  pythagtriplem8  14328  pythagtriplem9  14329  pythagtriplem19  14338  4sqlem10  14446  ram0  14521  isipodrs  15769  gsumval2  15885  mulgnn  16126  sylow1lem1  16596  gsumval3eu  16885  abvtrivd  17467  00lss  17566  lvecvscan2  17736  fidomndrng  17934  mvridlemOLD  18053  mvrcl  18089  mplmon  18103  mplmonmul  18104  mplcoe3OLD  18107  mplcoe2OLD  18111  evlslem3  18161  coe1tmfv2  18294  cply1coe0  18319  cply1coe0bi  18320  prmirredlem  18500  prmirredlemOLD  18503  uvcff  18799  1marepvsma1  19062  mdetrsca2  19083  mdetrlin2  19086  mdetunilem2  19092  mdetunilem5  19095  mdetunilem6  19096  mdetunilem9  19099  maducoeval2  19119  gsummatr01lem3  19136  gsummatr01lem4  19137  gsummatr01  19138  m2cpm  19219  m2cpminvid2lem  19232  fvmptnn04ifa  19328  fvmptnn04ifb  19329  fvmptnn04ifc  19330  chfacffsupp  19334  chfacfscmul0  19336  chfacfscmulgsum  19338  chfacfpmmul0  19340  chfacfpmmulgsum  19342  conclo  19893  dissnlocfin  20007  ptpjpre2  20058  txindis  20112  snfil  20342  alexsublem  20521  tsmsfbas  20603  stdbdxmet  20995  dscmet  21070  xrsxmet  21291  iccpnfcnv  21421  cphsubrglem  21601  minveclem3b  21820  minveclem4a  21822  ovolicc1  21904  dvexp2  22334  lhop2  22393  deg1sublt  22488  ig1pval3  22552  dvply1  22656  plydiveu  22670  quotcan  22681  aaliou3lem9  22722  taylthlem2  22745  pserdvlem2  22799  abelthlem9  22811  logtayllem  23016  logtayl  23017  cxpef  23022  angrtmuld  23116  isosctrlem2  23129  isosctrlem3  23130  chordthmlem  23139  leibpilem2  23248  leibpi  23249  rlimcnp2  23272  efrlim  23275  vma1  23416  muinv  23445  lgsval2lem  23557  lgsval4  23567  lgsdir  23581  lgseisenlem4  23603  lgsquadlem1  23605  lgsquad2  23611  m1lgs  23613  2sqlem8a  23622  2sqlem8  23623  padicabv  23791  ostth1  23794  ostth3  23799  tgbtwnne  23857  tgbtwndiff  23873  tgcolg  23917  tgbtwnconn1lem3  23937  legso  23961  tglineeltr  23987  tglineintmo  23998  tglineneq  24000  coltr2  24004  colline  24006  miriso  24026  mirhl  24035  mirbtwnhl  24036  symquadlem  24042  krippenlem  24043  midexlem  24045  ragncol  24062  footex  24071  colperp  24079  colperpexlem3  24082  mideulem2  24084  opphllem  24085  midex  24087  opptgdim2  24093  lmieu  24126  axlowdimlem15  24235  axcontlem2  24244  axcontlem7  24249  isusgra0  24323  usgraop  24326  usgra1v  24366  cyclnspth  24607  clwwlkn0  24750  rusgra0edg  24931  eupath2lem1  24953  eupath2lem2  24954  eupath2lem3  24955  gxpval  25237  strlem6  27151  hstrlem6  27159  atssma  27273  chirredlem1  27285  znsqcld  27537  xaddeq0  27549  xlt2addrd  27554  gcdnncl  27583  divnumden2  27585  2sqcoprm  27612  2sqmod  27613  submomnd  27677  ornglmullt  27774  orngrmullt  27775  ofldchr  27781  suborng  27782  xrge0iifcnv  27892  xrge0iifcv  27893  xrge0iif1  27897  qqhval2lem  27939  qqhf  27944  qqhre  27975  logccne0OLD  27988  logccne0  27989  ballotlemirc  28447  sgnmul  28458  sgn0bi  28463  signswlid  28493  fz0n  29087  dfrdg2  29203  nobndup  29435  nobnddown  29436  dfrdg4  29575  broutsideof2  29747  outsidele  29757  rankeq1o  29803  limsucncmpi  29885  ivthALT  30128  fdc  30213  heibor1lem  30280  heiborlem4  30285  heiborlem6  30287  jm2.26lem3  30918  kelac1  30984  phisum  31135  lcmgcdlem  31188  refsum2cnlem1  31366  neneq  31383  oddfl  31408  xrlttri5d  31414  icoiccdif  31500  fmul01lt1lem1  31506  climrec  31517  limcperiod  31542  reclimc  31567  cncfiooicclem1  31603  cncfioobdlem  31606  dvmptdiv  31618  fperdvper  31619  dvdivbd  31624  ditgeqiooicc  31649  itgsincmulx  31663  itgioocnicc  31666  iblcncfioo  31667  stoweidlem35  31706  stoweidlem39  31710  stirlinglem5  31749  stirlinglem8  31752  dirkerper  31767  dirkercncflem2  31775  dirkercncflem4  31777  fourierdlem31  31809  fourierdlem34  31812  fourierdlem41  31819  fourierdlem42  31820  fourierdlem44  31822  fourierdlem48  31826  fourierdlem49  31827  fourierdlem53  31831  fourierdlem56  31834  fourierdlem58  31836  fourierdlem60  31838  fourierdlem61  31839  fourierdlem62  31840  fourierdlem65  31843  fourierdlem66  31844  fourierdlem73  31851  fourierdlem76  31854  fourierdlem79  31857  fourierdlem81  31859  fourierdlem82  31860  fourierdlem93  31871  fourierdlem103  31881  fourierdlem104  31882  sqwvfoura  31900  fourierswlem  31902  sineq0ALT  33470  bnj1523  33860  2atm  34991  lhpocnle  35480  lhp2at0nle  35499  trlval3  35652  cdleme18c  35758  cdlemg17b  36128  cdlemg17i  36135  dia2dimlem2  36532  dia2dimlem3  36533  dihord6apre  36723  dihatlat  36801  dochshpsat  36921  lcfrlem9  37017  mapdhval2  37193  hdmap1val2  37268  hdmap14lem4a  37341  hdmap14lem6  37343
  Copyright terms: Public domain W3C validator