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

Theorem neneqd 2605
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 2600 . 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 1405    =/= wne 2598
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 2600
This theorem is referenced by:  necon3ad  2613  necon2bi  2640  necon2i  2646  necon4i  2647  pm2.21ddne  2717  nelrdva  3258  disjprg  4390  0inp0  4565  onnseq  7047  sniffsupp  7902  ackbij1lem15  8645  ttukeylem7  8926  fpwwe2lem13  9049  canthnumlem  9055  canthp1lem2  9060  recgt0  10426  elnnz  10914  xrnemnf  11380  xrnepnf  11381  fzprval  11793  expnnval  12211  elprchashprn2  12508  relexpsucnnr  13005  relexp1g  13006  relexpuzrel  13032  sgnp  13070  ruclem12  14181  dvdsle  14238  sqgcd  14403  eucalgf  14419  eucalginv  14420  qredeu  14455  divgcdodd  14467  rpdvds  14472  divnumden  14488  divdenle  14489  oddprm  14546  pythagtriplem4  14550  pythagtriplem8  14554  pythagtriplem9  14555  pythagtriplem19  14564  4sqlem10  14672  ram0  14747  isipodrs  16113  gsumval2  16229  mulgnn  16470  sylow1lem1  16940  gsumval3eu  17229  abvtrivd  17807  00lss  17906  lvecvscan2  18076  fidomndrng  18274  mvridlemOLD  18393  mvrcl  18429  mplmon  18443  mplmonmul  18444  mplcoe3OLD  18447  mplcoe2OLD  18451  evlslem3  18501  coe1tmfv2  18634  cply1coe0  18659  cply1coe0bi  18660  prmirredlem  18828  uvcff  19116  1marepvsma1  19375  mdetrsca2  19396  mdetrlin2  19399  mdetunilem2  19405  mdetunilem5  19408  mdetunilem6  19409  mdetunilem9  19412  maducoeval2  19432  gsummatr01lem3  19449  gsummatr01lem4  19450  gsummatr01  19451  m2cpm  19532  m2cpminvid2lem  19545  fvmptnn04ifa  19641  fvmptnn04ifb  19642  fvmptnn04ifc  19643  chfacffsupp  19647  chfacfscmul0  19649  chfacfscmulgsum  19651  chfacfpmmul0  19653  chfacfpmmulgsum  19655  conclo  20206  dissnlocfin  20320  ptpjpre2  20371  txindis  20425  snfil  20655  alexsublem  20834  tsmsfbas  20916  stdbdxmet  21308  dscmet  21383  xrsxmet  21604  iccpnfcnv  21734  cphsubrglem  21914  minveclem3b  22133  minveclem4a  22135  ovolicc1  22217  dvexp2  22647  lhop2  22706  deg1sublt  22801  ig1pval3  22865  dvply1  22970  plydiveu  22984  quotcan  22995  aaliou3lem9  23036  taylthlem2  23059  pserdvlem2  23113  abelthlem9  23125  logccne0  23256  logtayllem  23332  logtayl  23333  cxpef  23338  angrtmuld  23465  isosctrlem2  23476  isosctrlem3  23477  chordthmlem  23486  leibpilem2  23595  leibpi  23596  rlimcnp2  23620  efrlim  23623  vma1  23819  muinv  23848  lgsval2lem  23960  lgsval4  23970  lgsdir  23984  lgseisenlem4  24006  lgsquadlem1  24008  lgsquad2  24014  m1lgs  24016  2sqlem8a  24025  2sqlem8  24026  padicabv  24194  ostth1  24197  ostth3  24202  tgbtwnne  24260  tgbtwndiff  24276  tgcolg  24322  tgbtwnconn1lem3  24342  legso  24367  tglineeltr  24394  tglineintmo  24405  tglineneq  24407  coltr2  24411  colline  24413  miriso  24433  mirhl  24442  mirbtwnhl  24443  symquadlem  24449  krippenlem  24450  midexlem  24452  ragncol  24469  footex  24478  colperp  24486  colperpexlem3  24489  mideulem2  24491  opphllem  24492  midex  24494  opptgdim2  24500  lmieu  24533  axlowdimlem15  24663  axcontlem2  24672  axcontlem7  24677  isusgra0  24751  usgraop  24754  usgra1v  24794  cyclnspth  25035  clwwlkn0  25178  rusgra0edg  25359  eupath2lem1  25381  eupath2lem2  25382  eupath2lem3  25383  gxpval  25661  strlem6  27574  hstrlem6  27582  atssma  27696  chirredlem1  27708  znsqcld  27994  xaddeq0  28000  xlt2addrd  28006  gcdnncl  28044  divnumden2  28046  2sqcoprm  28073  2sqmod  28074  submomnd  28138  ornglmullt  28236  orngrmullt  28237  ofldchr  28243  suborng  28244  xrge0iifcnv  28354  xrge0iifcv  28355  xrge0iif1  28359  qqhval2lem  28400  qqhf  28405  qqhre  28436  esumrnmpt2  28501  esumcvgre  28524  inelpisys  28588  carsgclctunlem2  28753  ballotlemirc  28962  sgnmul  28973  sgn0bi  28978  signswlid  29008  bnj1523  29441  fz0n  29924  dfrdg2  30002  nobndup  30147  nobnddown  30148  dfrdg4  30276  broutsideof2  30447  outsidele  30457  rankeq1o  30496  ivthALT  30550  limsucncmpi  30664  topdifinffinlem  31251  icorempt2  31255  fdc  31500  heibor1lem  31567  heiborlem4  31572  heiborlem6  31574  2atm  32524  lhpocnle  33013  lhp2at0nle  33032  trlval3  33185  cdleme18c  33291  cdlemg17b  33661  cdlemg17i  33668  dia2dimlem2  34065  dia2dimlem3  34066  dihord6apre  34256  dihatlat  34334  dochshpsat  34454  lcfrlem9  34550  mapdhval2  34726  hdmap1val2  34801  hdmap14lem4a  34874  hdmap14lem6  34876  jm2.26lem3  35285  kelac1  35351  phisum  35503  lcmgcdlem  36040  sineq0ALT  36748  refsum2cnlem1  36772  neneq  36785  oddfl  36813  xrlttri5d  36819  icoiccdif  36913  fmul01lt1lem1  36927  fprodn0f  36943  climrec  36958  limcperiod  36983  reclimc  37008  cncfiooicclem1  37045  cncfioobdlem  37048  dvmptdiv  37063  fperdvper  37064  dvdivbd  37069  ditgeqiooicc  37108  itgsincmulx  37122  itgioocnicc  37125  iblcncfioo  37126  stoweidlem35  37166  stoweidlem39  37170  stirlinglem5  37209  stirlinglem8  37212  dirkerper  37227  dirkercncflem2  37235  dirkercncflem4  37237  fourierdlem31  37269  fourierdlem34  37272  fourierdlem41  37279  fourierdlem42  37280  fourierdlem44  37282  fourierdlem48  37286  fourierdlem49  37287  fourierdlem53  37291  fourierdlem56  37294  fourierdlem58  37296  fourierdlem60  37298  fourierdlem61  37299  fourierdlem62  37300  fourierdlem65  37303  fourierdlem66  37304  fourierdlem73  37311  fourierdlem76  37314  fourierdlem79  37317  fourierdlem81  37319  fourierdlem82  37320  fourierdlem93  37331  fourierdlem103  37341  fourierdlem104  37342  sqwvfoura  37360  fourierswlem  37362  elaa2lem  37365  elaa2  37366  etransclem4  37370  etransclem24  37390  etransclem31  37397  etransclem32  37398  etransclem35  37401  divgcdoddALTV  37745  dignn0flhalflem1  38727
  Copyright terms: Public domain W3C validator