Theorem neneqd 2930

Description: Deduction eliminating inequality definition. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
neneqd.1	⊢ (𝜑 → 𝐴 ≠ 𝐵)

Assertion

Ref	Expression
neneqd	⊢ (𝜑 → ¬ 𝐴 = 𝐵)

Proof of Theorem neneqd

Step	Hyp	Ref	Expression
1		neneqd.1	. 2 ⊢ (𝜑 → 𝐴 ≠ 𝐵)
2		df-ne 2926	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	sylib 218	1 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2925

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 207  df-ne 2926

This theorem is referenced by:  neneq  2931  necon2bi  2955  necon2i  2959  necon4i  2960  pm2.21ddne  3009  mteqand  3016  nelrdva  3665  eldifsnneq  4742  disjprg  5088  0inp0  5298  rnmptn0  6193  resf1extb  7867  frxp2  8077  frxp3  8084  onnseq  8267  finnzfsuppd  9263  sniffsupp  9290  dfac2b  10025  ackbij1lem15  10127  ttukeylem7  10409  fpwwe2lem12  10536  canthnumlem  10542  canthp1lem2  10547  recgt0  11970  nnneneg  12163  elnnz  12481  xrnemnf  13019  xrnepnf  13020  fzprval  13488  fzodisjsn  13600  expnnval  13971  znsqcld  14069  hashelne0d  14275  elprchashprn2  14303  relexpsucnnr  14932  relexp1g  14933  relexpuzrel  14959  sgnp  14997  fprodn0f  15898  ruclem12  16150  dvdsle  16221  nndvdslegcd  16416  gcdnncl  16418  divgcdnn  16426  nn0rppwr  16472  sqgcd  16473  eucalgf  16494  eucalginv  16495  lcmgcdlem  16517  lcmftp  16547  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  qredeu  16569  rpdvds  16571  cncongr2  16579  divnumden  16659  divdenle  16660  phisum  16702  oddprm  16722  pythagtriplem4  16731  pythagtriplem8  16735  pythagtriplem9  16736  4sqlem10  16859  ram0  16934  cat1lem  18003  isipodrs  18443  gsumval2  18560  smndex1n0mnd  18786  smndex2dnrinv  18789  mulgnn  18954  sylow1lem1  19477  gsumval3eu  19783  ablsimpgfindlem1  19988  ablsimpgfindlem2  19989  ablsimpgfind  19991  fincygsubgodd  19993  submomnd  20011  rrgnz  20589  fidomndrng  20658  abvtrivd  20717  ornglmullt  20754  orngrmullt  20755  suborng  20761  00lss  20844  lvecvscan2  21019  prmirredlem  21379  ofldchr  21483  uvcff  21698  mvrcl  21899  mplmon  21940  mplmonmul  21941  psdmul  22051  coe1tmfv2  22159  cply1coe0  22186  cply1coe0bi  22187  1marepvsma1  22468  mdetrsca2  22489  mdetrlin2  22492  mdetunilem2  22498  mdetunilem5  22501  mdetunilem6  22502  mdetunilem9  22505  maducoeval2  22525  gsummatr01lem3  22542  gsummatr01lem4  22543  gsummatr01  22544  m2cpm  22626  m2cpminvid2lem  22639  fvmptnn04ifa  22735  fvmptnn04ifb  22736  fvmptnn04ifc  22737  chfacffsupp  22741  chfacfscmul0  22743  chfacfscmulgsum  22745  chfacfpmmul0  22747  chfacfpmmulgsum  22749  connclo  23300  dissnlocfin  23414  ptpjpre2  23465  txindis  23519  snfil  23749  alexsublem  23929  tsmsfbas  24013  stdbdxmet  24401  dscmet  24458  xrsxmet  24696  iccpnfcnv  24840  cphsubrglem  25075  minveclem3b  25326  minveclem4a  25328  ovolicc1  25415  dvexp2  25856  dvmptdiv  25876  lhop2  25918  deg1sublt  26013  ig1pval3  26081  dvply1  26189  plydiveu  26204  quotcan  26215  aaliou3lem9  26256  taylthlem2  26280  taylthlem2OLD  26281  pserdvlem2  26336  abelthlem9  26348  logccne0  26485  logtayllem  26566  logtayl  26567  cxpef  26572  rtprmirr  26668  angrtmuld  26716  isosctrlem3  26728  chordthmlem  26740  leibpilem2  26849  leibpi  26850  rlimcnp2  26874  efrlim  26877  efrlimOLD  26878  vma1  27074  muinv  27101  lgsval2lem  27216  lgsval4  27226  lgsdir  27241  lgseisenlem4  27287  lgsquadlem1  27289  lgsquad2  27295  m1lgs  27297  2sqlem8a  27334  2sqlem8  27335  2sqcoprm  27344  2sqmod  27345  padicabv  27539  ostth1  27542  ostth3  27547  nolesgn2ores  27582  nogesgn1ores  27584  nosep1o  27591  nosep2o  27592  nosepdmlem  27593  nosepssdm  27596  noresle  27607  nosupbnd1lem3  27620  nosupbnd1lem4  27621  nosupbnd1lem5  27622  nosupbnd1lem6  27623  nosupbnd2lem1  27625  noinfbnd1lem3  27635  noinfbnd1lem4  27636  noinfbnd1lem5  27637  noinfbnd1lem6  27638  noinfbnd2lem1  27640  0elold  27824  elnnzs  28294  expsnnval  28318  expsne0  28328  tgbtwnne  28435  tgbtwndiff  28451  tgcolg  28499  tgbtwnconn1lem3  28519  legso  28544  tglineeltr  28576  tglineintmo  28587  tglineneq  28589  colline  28594  mirne  28612  miriso  28615  mirhl  28624  mirbtwnhl  28625  symquadlem  28634  krippenlem  28635  midexlem  28637  ragncol  28654  footexALT  28663  footexlem2  28665  colperp  28674  colperpexlem3  28677  mideulem2  28679  opphllem  28680  midex  28682  opptgdim2  28690  oppperpex  28698  hlpasch  28701  colopp  28714  lmieu  28729  trgcopy  28749  cgracol  28773  cgrg3col4  28798  axlowdimlem15  28901  axcontlem2  28910  axcontlem7  28915  1egrvtxdg0  29457  2pthnloop  29676  cyclnspth  29746  eupth2lem1  30162  eupth2lem2  30163  eupth2lem3lem6  30177  nrt2irr  30417  strlem6  32200  hstrlem6  32208  atssma  32322  chirredlem1  32334  snsssng  32458  ifnetrue  32491  ifnefals  32492  fmptunsnop  32643  xaddeq0  32697  rexmul2  32698  xlt2addrd  32703  xnn0nn0d  32716  fzone1  32744  hashpss  32755  elq2  32757  divnumden2  32761  sgnmul  32781  sgn0bi  32786  2exple2exp  32791  chnub  32955  pmtridf1o  33037  pmtridfv1  33038  pmtridfv2  33039  elrgspnlem2  33184  elrgspnlem3  33185  fracfld  33248  pidlnz  33314  lindssn  33316  drngidl  33371  drngidlhash  33372  0ringprmidl  33387  qsidomlem1  33390  ssdifidlprm  33396  mxidlmaxv  33406  mxidlprm  33408  mxidlirredi  33409  mxidlirred  33410  krull  33417  rsprprmprmidlb  33461  rprmasso2  33464  pidufd  33481  1arithufdlem3  33484  dfufd2  33488  zringidom  33489  0ringmon1p  33493  ig1pnunit  33534  lindsunlem  33597  fldextrspundgdvdslem  33653  fldext2rspun  33655  ply1annnr  33676  fldext2chn  33701  constrextdg2lem  33721  constrext2chnlem  33723  constrcon  33747  2sqr3minply  33753  cos9thpiminply  33761  1smat1  33777  submatminr1  33783  madjusmdetlem2  33801  zarcls1  33842  zarclsint  33845  zarclssn  33846  xrge0iifcnv  33906  xrge0iifcv  33907  xrge0iif1  33911  qqhval2lem  33954  qqhf  33959  qqhre  33993  esumrnmpt2  34041  esumcvgre  34064  inelpisys  34127  carsgclctunlem2  34293  ballotlemirc  34506  signswlid  34533  repr0  34585  reprlt  34593  reprgt  34595  reprinfz1  34596  tgoldbachgtda  34635  tgoldbachgt  34637  bnj1523  35044  acycgr2v  35133  fmlaomn0  35373  fmlasucdisj  35382  fz0n  35714  dfrdg2  35779  dfrdg4  35935  broutsideof2  36106  outsidele  36116  rankeq1o  36155  ivthALT  36319  limsucncmpi  36429  topdifinffinlem  37331  icorempo  37335  finxpreclem2  37374  finxp1o  37376  finxpreclem6  37380  poimirlem9  37619  poimirlem11  37621  poimirlem12  37622  poimirlem25  37635  fdc  37735  heibor1lem  37799  heiborlem4  37804  heiborlem6  37806  disjressuc2  38370  2atm  39516  lhpocnle  40005  lhp2at0nle  40024  trlval3  40176  cdleme18c  40282  cdlemg17b  40651  cdlemg17i  40658  dia2dimlem2  41054  dia2dimlem3  41055  dihord6apre  41245  dihatlat  41323  dochshpsat  41443  lcfrlem9  41539  mapdhval2  41715  hdmap1val2  41789  hdmap14lem4a  41860  hdmap14lem6  41862  dvrelogpow2b  42051  aks4d1p1p4  42054  aks4d1p6  42064  fldhmf1  42073  primrootspoweq0  42089  aks6d1c2p2  42102  hashscontpow  42105  aks6d1c5  42122  sticksstones1  42129  sticksstones10  42138  sticksstones12a  42140  sticksstones12  42141  sticksstones22  42151  aks6d1c6lem4  42156  aks6d1c7lem1  42163  aks6d1c7  42167  aks5lem8  42184  negn0nposznnd  42265  mhpind  42577  prjspner1  42609  dffltz  42617  3cubeslem2  42668  jm2.26lem3  42984  kelac1  43046  cantnfresb  43307  tfsconcat0b  43329  nlimsuc  43424  clsk1indlem0  44024  scotteld  44229  sineq0ALT  44920  refsum2cnlem1  45025  disjxp1  45057  nelrnmpt  45072  disjf1  45171  disjrnmpt2  45176  disjinfi  45180  oddfl  45270  xrlttri5d  45276  supxrge  45328  nepnfltpnf  45332  nemnftgtmnft  45334  xrlexaddrp  45342  xrred  45354  supminfxr2  45458  icoiccdif  45515  qinioo  45526  ioonct  45528  fmul01lt1lem1  45575  climrec  45594  limcperiod  45619  reclimc  45644  limsupub  45695  liminflbuz2  45806  cncfiooicclem1  45884  cncfioobdlem  45887  fperdvper  45910  dvdivbd  45914  ditgeqiooicc  45951  itgsincmulx  45965  itgioocnicc  45968  iblcncfioo  45969  stoweidlem35  46026  stoweidlem39  46030  stirlinglem5  46069  stirlinglem8  46072  dirkerper  46087  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem31  46129  fourierdlem34  46132  fourierdlem41  46139  fourierdlem42  46140  fourierdlem44  46142  fourierdlem48  46145  fourierdlem49  46146  fourierdlem53  46150  fourierdlem56  46153  fourierdlem58  46155  fourierdlem60  46157  fourierdlem61  46158  fourierdlem62  46159  fourierdlem65  46162  fourierdlem66  46163  fourierdlem73  46170  fourierdlem76  46173  fourierdlem79  46176  fourierdlem81  46178  fourierdlem82  46179  fourierdlem93  46190  fourierdlem103  46200  fourierdlem104  46201  sqwvfoura  46219  fourierswlem  46221  elaa2lem  46224  elaa2  46225  etransclem4  46229  etransclem24  46249  etransclem31  46256  etransclem32  46257  etransclem35  46260  sge0repnf  46377  sge0fodjrnlem  46407  sge0iunmpt  46409  sge0rpcpnf  46412  nnfoctbdjlem  46446  meadjun  46453  voliunsge0lem  46463  hoicvr  46539  ovnn0val  46542  ovnsubaddlem1  46561  hoidmvn0val  46575  hsphoidmvle  46577  hoidmv1lelem1  46582  hoidmv1lelem2  46583  hoidmv1lelem3  46584  ovnhoilem1  46592  ovnsubadd2lem  46636  ovnovollem3  46649  cjnpoly  46883  lighneallem3  47601  divgcdoddALTV  47676  isubgr0uhgr  47867  usgrexmpl2trifr  48031  gpg5nbgrvtx03star  48074  gpg5nbgr3star  48075  dignn0flhalflem1  48610  itcoval2  48659  itcoval3  48660  itcovalsuc  48662  ackvalsuc1mpt  48673  line2xlem  48748