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

Theorem neneqd 2640
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 2635 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2sylib 201 1  |-  ( ph  ->  -.  A  =  B )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1455    =/= wne 2633
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 190  df-ne 2635
This theorem is referenced by:  neneq  2641  necon3ad  2649  necon2bi  2666  necon2i  2670  necon4i  2671  pm2.21ddne  2720  nelrdva  3261  disjprg  4414  0inp0  4592  onnseq  7094  sniffsupp  7954  ackbij1lem15  8695  ttukeylem7  8976  fpwwe2lem13  9098  canthnumlem  9104  canthp1lem2  9109  recgt0  10482  elnnz  10981  xrnemnf  11453  xrnepnf  11454  fzprval  11891  expnnval  12313  elprchashprn2  12611  relexpsucnnr  13143  relexp1g  13144  relexpuzrel  13170  sgnp  13208  fprodn0f  14100  ruclem12  14348  dvdsle  14405  nndvdslegcd  14534  gcdnncl  14536  sqgcd  14581  eucalgf  14597  eucalginv  14598  lcmgcdlem  14626  lcmftp  14664  lcmfunsnlem2lem1  14666  lcmfunsnlem2lem2  14667  divgcdodd  14708  qredeu  14719  rpdvds  14731  divnumden  14752  divdenle  14753  oddprm  14820  pythagtriplem4  14824  pythagtriplem8  14828  pythagtriplem9  14829  pythagtriplem19  14838  4sqlem10  14946  ram0  15035  isipodrs  16462  gsumval2  16578  mulgnn  16819  sylow1lem1  17305  gsumval3eu  17593  abvtrivd  18123  00lss  18220  lvecvscan2  18390  fidomndrng  18586  mvrcl  18728  mplmon  18742  mplmonmul  18743  evlslem3  18792  coe1tmfv2  18923  cply1coe0  18948  cply1coe0bi  18949  prmirredlem  19119  uvcff  19404  1marepvsma1  19663  mdetrsca2  19684  mdetrlin2  19687  mdetunilem2  19693  mdetunilem5  19696  mdetunilem6  19697  mdetunilem9  19700  maducoeval2  19720  gsummatr01lem3  19737  gsummatr01lem4  19738  gsummatr01  19739  m2cpm  19820  m2cpminvid2lem  19833  fvmptnn04ifa  19929  fvmptnn04ifb  19930  fvmptnn04ifc  19931  chfacffsupp  19935  chfacfscmul0  19937  chfacfscmulgsum  19939  chfacfpmmul0  19941  chfacfpmmulgsum  19943  conclo  20485  dissnlocfin  20599  ptpjpre2  20650  txindis  20704  snfil  20934  alexsublem  21114  tsmsfbas  21197  stdbdxmet  21585  dscmet  21642  xrsxmet  21882  iccpnfcnv  22027  cphsubrglem  22210  minveclem3b  22425  minveclem4a  22427  minveclem3bOLD  22437  minveclem4aOLD  22439  ovolicc1  22524  dvexp2  22964  lhop2  23023  deg1sublt  23115  ig1pval3  23182  ig1pval3OLD  23188  dvply1  23293  plydiveu  23307  quotcan  23318  aaliou3lem9  23362  taylthlem2  23385  pserdvlem2  23439  abelthlem9  23451  logccne0  23584  logtayllem  23660  logtayl  23661  cxpef  23666  angrtmuld  23793  isosctrlem2  23804  isosctrlem3  23805  chordthmlem  23814  leibpilem2  23923  leibpi  23924  rlimcnp2  23948  efrlim  23951  vma1  24149  muinv  24178  lgsval2lem  24290  lgsval4  24300  lgsdir  24314  lgseisenlem4  24336  lgsquadlem1  24338  lgsquad2  24344  m1lgs  24346  2sqlem8a  24355  2sqlem8  24356  padicabv  24524  ostth1  24527  ostth3  24532  tgbtwnne  24590  tgbtwndiff  24606  tgcolg  24655  tgbtwnconn1lem3  24675  legso  24700  tglineeltr  24732  tglineintmo  24743  tglineneq  24745  colline  24750  mirne  24768  miriso  24771  mirhl  24780  mirbtwnhl  24781  symquadlem  24790  krippenlem  24791  midexlem  24793  ragncol  24810  footex  24819  colperp  24827  colperpexlem3  24830  mideulem2  24832  opphllem  24833  midex  24835  opptgdim2  24843  oppperpex  24851  hlpasch  24854  colopp  24867  colhp  24868  lmieu  24882  trgcopy  24902  cgracol  24925  cgrg3col4  24940  axlowdimlem15  25042  axcontlem2  25051  axcontlem7  25056  isusgra0  25130  usgraop  25133  usgra1v  25173  cyclnspth  25415  clwwlkn0  25558  rusgra0edg  25739  eupath2lem1  25761  eupath2lem2  25762  eupath2lem3  25763  gxpval  26043  strlem6  27965  hstrlem6  27973  atssma  28087  chirredlem1  28099  znsqcld  28375  xaddeq0  28382  xlt2addrd  28390  divnumden2  28433  2sqcoprm  28460  2sqmod  28461  submomnd  28524  ornglmullt  28621  orngrmullt  28622  ofldchr  28628  suborng  28629  1smat1  28681  submatminr1  28687  madjusmdetlem2  28705  xrge0iifcnv  28790  xrge0iifcv  28791  xrge0iif1  28795  qqhval2lem  28836  qqhf  28841  qqhre  28875  esumrnmpt2  28940  esumcvgre  28963  inelpisys  29027  carsgclctunlem2  29201  ballotlemirc  29414  ballotlemircOLD  29452  sgnmul  29463  sgn0bi  29468  signswlid  29498  bnj1523  29930  fz0n  30414  dfrdg2  30492  nobndup  30639  nobnddown  30640  dfrdg4  30768  broutsideof2  30939  outsidele  30949  rankeq1o  30988  ivthALT  31041  limsucncmpi  31155  topdifinffinlem  31796  icorempt2  31800  finxpreclem2  31828  finxp1o  31830  finxpreclem6  31834  poimirlem9  31995  poimirlem11  31997  poimirlem12  31998  poimirlem25  32011  fdc  32120  heibor1lem  32187  heiborlem4  32192  heiborlem6  32194  2atm  33138  lhpocnle  33627  lhp2at0nle  33646  trlval3  33799  cdleme18c  33905  cdlemg17b  34275  cdlemg17i  34282  dia2dimlem2  34679  dia2dimlem3  34680  dihord6apre  34870  dihatlat  34948  dochshpsat  35068  lcfrlem9  35164  mapdhval2  35340  hdmap1val2  35415  hdmap14lem4a  35488  hdmap14lem6  35490  jm2.26lem3  35902  kelac1  35967  phisum  36122  sineq0ALT  37375  refsum2cnlem1  37399  disjxp1  37450  nelrnmpt  37473  disjf1  37511  disjrnmpt2  37517  disjinfi  37522  oddfl  37562  xrlttri5d  37568  supxrge  37636  nepnfltpnf  37640  nemnftgtmnft  37642  xrlexaddrp  37650  xrred  37664  icoiccdif  37710  qinioo  37722  ioonct  37724  fmul01lt1lem1  37748  climrec  37767  limcperiod  37794  reclimc  37820  cncfiooicclem1  37857  cncfioobdlem  37860  dvmptdiv  37875  fperdvper  37876  dvdivbd  37881  ditgeqiooicc  37923  itgsincmulx  37937  itgioocnicc  37940  iblcncfioo  37941  stoweidlem35  37997  stoweidlem39  38001  stirlinglem5  38041  stirlinglem8  38044  dirkerper  38059  dirkercncflem2  38067  dirkercncflem4  38069  fourierdlem31  38101  fourierdlem31OLD  38102  fourierdlem34  38105  fourierdlem41  38112  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem44  38116  fourierdlem48  38119  fourierdlem49  38120  fourierdlem53  38124  fourierdlem56  38127  fourierdlem58  38129  fourierdlem60  38131  fourierdlem61  38132  fourierdlem62  38133  fourierdlem65  38136  fourierdlem66  38137  fourierdlem73  38144  fourierdlem76  38147  fourierdlem79  38150  fourierdlem81  38152  fourierdlem82  38153  fourierdlem93  38164  fourierdlem103  38174  fourierdlem104  38175  sqwvfoura  38193  fourierswlem  38195  elaa2lem  38198  elaa2lemOLD  38199  elaa2  38200  etransclem4  38204  etransclem24  38224  etransclem31  38231  etransclem32  38232  etransclem35  38235  sge0repnf  38331  sge0fodjrnlem  38361  sge0iunmpt  38363  sge0rpcpnf  38366  nnfoctbdjlem  38398  meadjun  38405  voliunsge0lem  38415  hoicvr  38477  ovnn0val  38480  ovnsubaddlem1  38499  hoidmvn0val  38513  hsphoidmvle  38515  hoidmv1lelem1  38520  hoidmv1lelem2  38521  hoidmv1lelem3  38522  ovnhoilem1  38530  ovnsubadd2lem  38574  ovnovollem3  38587  divgcdoddALTV  38946  usgr1vr  39475  2pthnloop  39860  cyclnsPth  39918  dignn0flhalflem1  40795
  Copyright terms: Public domain W3C validator