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

Theorem neneqd 2627
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 2622 . 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 1369    =/= wne 2620
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 2622
This theorem is referenced by:  necon2bi  2681  necon2i  2682  pm2.21ddne  2709  nelrdva  3189  disjprg  4309  0inp0  4485  onnseq  6826  sniffsupp  7680  ackbij1lem15  8424  ttukeylem7  8705  fpwwe2lem13  8830  canthnumlem  8836  canthp1lem2  8841  recgt0  10194  elnnz  10677  xrnemnf  11120  xrnepnf  11121  fzprval  11538  expnnval  11889  elprchashprn2  12177  sgnp  12600  ruclem12  13544  dvdsle  13599  sqgcd  13763  eucalgf  13779  eucalginv  13780  qredeu  13814  divgcdodd  13826  rpdvds  13831  divnumden  13847  divdenle  13848  oddprm  13903  pythagtriplem4  13907  pythagtriplem8  13911  pythagtriplem9  13912  pythagtriplem19  13921  4sqlem10  14029  ram0  14104  isipodrs  15352  gsumval2  15534  mulgnn  15654  sylow1lem1  16118  gsumval3eu  16402  abvtrivd  16947  00lss  17045  lvecvscan2  17215  fidomndrng  17401  mvridlemOLD  17514  mvrcl  17550  mplmon  17564  mplmonmul  17565  mplcoe3OLD  17568  mplcoe2OLD  17572  evlslem3  17622  coe1tmfv2  17750  prmirredlem  17939  prmirredlemOLD  17942  uvcff  18238  1marepvsma1  18416  mdet1  18430  mdetrsca2  18433  mdetrlin2  18435  mdetunilem2  18441  mdetunilem6  18445  mdetunilem9  18448  maducoeval2  18468  gsummatr01lem3  18485  gsummatr01lem4  18486  gsummatr01  18487  conclo  19041  ptpjpre2  19175  txindis  19229  snfil  19459  alexsublem  19638  tsmsfbas  19720  stdbdxmet  20112  dscmet  20187  xrsxmet  20408  iccpnfcnv  20538  cphsubrglem  20718  minveclem3b  20937  minveclem4a  20939  ovolicc1  21021  dvexp2  21450  lhop2  21509  deg1sublt  21604  ig1pval3  21668  dvply1  21772  plydiveu  21786  quotcan  21797  aaliou3lem9  21838  taylthlem2  21861  pserdvlem2  21915  abelthlem9  21927  logtayllem  22126  logtayl  22127  cxpef  22132  angrtmuld  22226  isosctrlem2  22239  isosctrlem3  22240  chordthmlem  22249  leibpilem2  22358  leibpi  22359  rlimcnp2  22382  efrlim  22385  vma1  22526  muinv  22555  lgsval2lem  22667  lgsval4  22677  lgsdir  22691  lgseisenlem4  22713  lgsquadlem1  22715  lgsquad2  22721  m1lgs  22723  2sqlem8a  22732  2sqlem8  22733  padicabv  22901  ostth1  22904  ostth3  22909  tgbtwndiff  22981  tgcolg  23010  tgbtwnconn1lem3  23028  tglineeltr  23059  tglineintmo  23069  tglineneq  23071  colline  23074  miriso  23095  symquadlem  23105  krippenlem  23106  midexlem  23108  ragncol  23124  footex  23131  axlowdimlem15  23224  axcontlem2  23233  axcontlem7  23238  isusgra0  23297  usgra1v  23330  cyclnspth  23539  eupath2lem1  23620  eupath2lem2  23621  eupath2lem3  23622  gxpval  23768  strlem6  25682  hstrlem6  25690  atssma  25804  chirredlem1  25816  xaddeq0  26068  xlt2addrd  26073  divnumden2  26109  submomnd  26195  ornglmullt  26297  orngrmullt  26298  ofldchr  26304  suborng  26305  xrge0iifcnv  26385  xrge0iifcv  26386  xrge0iif1  26390  qqhval2lem  26432  qqhf  26437  qqhre  26468  logccne0OLD  26476  logccne0  26477  ballotlemirc  26936  sgnmul  26947  sgnsub  26949  sgn0bi  26952  sgnmulsgn  26954  sgnmulsgp  26955  signswlid  26982  fz0n  27411  dfrdg2  27631  nobndup  27863  nobnddown  27864  dfrdg4  28003  broutsideof2  28175  outsidele  28185  rankeq1o  28231  limsucncmpi  28313  ivthALT  28556  fdc  28667  heibor1lem  28734  heiborlem4  28739  heiborlem6  28741  jm2.26lem3  29376  kelac1  29442  phisum  29593  refsum2cnlem1  29785  fmul01lt1lem1  29791  climrec  29802  stoweidlem35  29856  stoweidlem39  29860  stirlinglem5  29899  stirlinglem8  29902  clwwlkn0  30463  rusgra0edg  30599  cply1coe0  30882  cply1coe0bi  30883  mat2cnstpmat  31092  m2pminv2lem  31100  sineq0ALT  31769  bnj1523  32158  2atm  33267  lhpocnle  33756  lhp2at0nle  33775  trlval3  33927  cdleme18c  34033  cdlemg17b  34402  cdlemg17i  34409  dia2dimlem2  34806  dia2dimlem3  34807  dihord6apre  34997  dihatlat  35075  dochshpsat  35195  lcfrlem9  35291  mapdhval2  35467  hdmap1val2  35542  hdmap14lem4a  35615  hdmap14lem6  35617
  Copyright terms: Public domain W3C validator