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

Theorem neneqd 2617
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 2601 . 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 1652    =/= wne 2599
This theorem is referenced by:  necon2bi  2650  necon2i  2651  pm2.21ddne  2678  nelrdva  3143  disjprg  4208  0inp0  4371  onnseq  6606  ackbij1lem15  8114  ttukeylem7  8395  fpwwe2lem13  8517  canthnumlem  8523  canthp1lem2  8528  recgt0  9854  elnnz  10292  xrnemnf  10718  xrnepnf  10719  fzprval  11106  expnnval  11385  elprchashprn2  11667  ruclem12  12840  dvdsle  12895  sqgcd  13058  eucalgf  13074  eucalginv  13075  qredeu  13107  divgcdodd  13119  rpdvds  13124  divnumden  13140  divdenle  13141  oddprm  13189  pythagtriplem4  13193  pythagtriplem8  13197  pythagtriplem9  13198  pythagtriplem19  13207  4sqlem10  13315  ram0  13390  isipodrs  14587  gsumval2  14783  mulgnn  14896  sylow1lem1  15232  gsumval3eu  15513  abvtrivd  15928  00lss  16018  lvecvscan2  16184  fidomndrng  16367  mvridlem  16483  mvrcl  16512  mplmon  16526  mplmonmul  16527  mplcoe3  16529  mplcoe2  16530  coe1tmfv2  16667  prmirredlem  16773  conclo  17478  ptpjpre2  17612  txindis  17666  snfil  17896  alexsublem  18075  tsmsfbas  18157  stdbdxmet  18545  dscmet  18620  xrsxmet  18840  iccpnfcnv  18969  cphsubrglem  19140  minveclem3b  19329  minveclem4a  19331  ovolicc1  19412  dvexp2  19840  lhop2  19899  evlslem3  19935  deg1sublt  20033  ig1pval3  20097  dvply1  20201  plydiveu  20215  quotcan  20226  aaliou3lem9  20267  taylthlem2  20290  pserdvlem2  20344  abelthlem9  20356  logtayllem  20550  logtayl  20551  cxpef  20556  angrtmuld  20650  isosctrlem2  20663  isosctrlem3  20664  chordthmlem  20673  leibpilem2  20781  leibpi  20782  rlimcnp2  20805  efrlim  20808  vma1  20949  muinv  20978  lgsval2lem  21090  lgsval4  21100  lgsdir  21114  lgseisenlem4  21136  lgsquadlem1  21138  lgsquad2  21144  m1lgs  21146  2sqlem8a  21155  2sqlem8  21156  padicabv  21324  ostth1  21327  ostth3  21332  isusgra0  21376  usgra1v  21409  cyclnspth  21618  eupath2lem1  21699  eupath2lem2  21700  eupath2lem3  21701  gxpval  21847  strlem6  23759  hstrlem6  23767  atssma  23881  chirredlem1  23893  xaddeq0  24119  xlt2addrd  24124  divnumden2  24161  ofldchr  24244  subofld  24245  xrge0iifcnv  24319  xrge0iifcv  24320  xrge0iif1  24324  qqhval2lem  24365  qqhf  24370  qqhre  24386  logccne0OLD  24395  logccne0  24396  ballotlemirc  24789  fz0n  25202  dfrdg2  25423  nobndup  25655  nobnddown  25656  dfrdg4  25795  axlowdimlem15  25895  axcontlem2  25904  axcontlem7  25909  broutsideof2  26056  outsidele  26066  rankeq1o  26112  limsucncmpi  26195  ivthALT  26338  fdc  26449  heibor1lem  26518  heiborlem4  26523  heiborlem6  26525  jm2.26lem3  27072  kelac1  27138  mamulid  27435  mamurid  27436  phisum  27495  refsum2cnlem1  27684  fmul01lt1lem1  27690  climrec  27705  stoweidlem35  27760  stoweidlem39  27764  stirlinglem5  27803  stirlinglem8  27806  frgra2v  28389  sgnp  28520  sineq0ALT  29049  bnj1523  29440  2atm  30324  lhpocnle  30813  lhp2at0nle  30832  trlval3  30984  cdleme18c  31090  cdlemg17b  31459  cdlemg17i  31466  dia2dimlem2  31863  dia2dimlem3  31864  dihord6apre  32054  dihatlat  32132  dochshpsat  32252  lcfrlem9  32348  mapdhval2  32524  hdmap1val2  32599  hdmap14lem4a  32672  hdmap14lem6  32674
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 2601
  Copyright terms: Public domain W3C validator