Theorem neneqd 2949

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 2945	. 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵)
3	1, 2	sylib 217	1 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2944

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 206  df-ne 2945

This theorem is referenced by:  neneq  2950  necon2bi  2975  necon2i  2979  necon4i  2980  pm2.21ddne  3030  mteqand  3049  nelrdva  3641  eldifsnneq  4725  disjprg  5071  0inp0  5282  rnmptn0  6152  onnseq  8184  sniffsupp  9168  dfac2b  9895  ackbij1lem15  9999  ttukeylem7  10280  fpwwe2lem12  10407  canthnumlem  10413  canthp1lem2  10418  recgt0  11830  nnneneg  12017  elnnz  12338  xrnemnf  12862  xrnepnf  12863  fzprval  13326  fzodisjsn  13434  expnnval  13794  znsqcld  13889  hashelne0d  14092  elprchashprn2  14120  relexpsucnnr  14745  relexp1g  14746  relexpuzrel  14772  sgnp  14810  fprodn0f  15710  ruclem12  15959  dvdsle  16028  nndvdslegcd  16221  gcdnncl  16223  divgcdnn  16231  sqgcd  16279  eucalgf  16297  eucalginv  16298  lcmgcdlem  16320  lcmftp  16350  lcmfunsnlem2lem1  16352  lcmfunsnlem2lem2  16353  qredeu  16372  rpdvds  16374  cncongr2  16382  divnumden  16461  divdenle  16462  phisum  16500  oddprm  16520  pythagtriplem4  16529  pythagtriplem8  16533  pythagtriplem9  16534  4sqlem10  16657  ram0  16732  cat1lem  17820  isipodrs  18264  gsumval2  18379  smndex1n0mnd  18560  smndex2dnrinv  18563  mulgnn  18717  sylow1lem1  19212  gsumval3eu  19514  ablsimpgfindlem1  19719  ablsimpgfindlem2  19720  ablsimpgfind  19722  fincygsubgodd  19724  abvtrivd  20109  00lss  20212  lvecvscan2  20383  fidomndrng  20588  prmirredlem  20703  uvcff  21007  mvrcl  21230  mplmon  21245  mplmonmul  21246  coe1tmfv2  21455  cply1coe0  21479  cply1coe0bi  21480  1marepvsma1  21741  mdetrsca2  21762  mdetrlin2  21765  mdetunilem2  21771  mdetunilem5  21774  mdetunilem6  21775  mdetunilem9  21778  maducoeval2  21798  gsummatr01lem3  21815  gsummatr01lem4  21816  gsummatr01  21817  m2cpm  21899  m2cpminvid2lem  21912  fvmptnn04ifa  22008  fvmptnn04ifb  22009  fvmptnn04ifc  22010  chfacffsupp  22014  chfacfscmul0  22016  chfacfscmulgsum  22018  chfacfpmmul0  22020  chfacfpmmulgsum  22022  connclo  22575  dissnlocfin  22689  ptpjpre2  22740  txindis  22794  snfil  23024  alexsublem  23204  tsmsfbas  23288  stdbdxmet  23680  dscmet  23737  xrsxmet  23981  iccpnfcnv  24116  cphsubrglem  24350  minveclem3b  24601  minveclem4a  24603  ovolicc1  24689  dvexp2  25127  dvmptdiv  25147  lhop2  25188  deg1sublt  25284  ig1pval3  25348  dvply1  25453  plydiveu  25467  quotcan  25478  aaliou3lem9  25519  taylthlem2  25542  pserdvlem2  25596  abelthlem9  25608  logccne0  25743  logtayllem  25823  logtayl  25824  cxpef  25829  angrtmuld  25967  isosctrlem3  25979  chordthmlem  25991  leibpilem2  26100  leibpi  26101  rlimcnp2  26125  efrlim  26128  vma1  26324  muinv  26351  lgsval2lem  26464  lgsval4  26474  lgsdir  26489  lgseisenlem4  26535  lgsquadlem1  26537  lgsquad2  26543  m1lgs  26545  2sqlem8a  26582  2sqlem8  26583  2sqcoprm  26592  2sqmod  26593  padicabv  26787  ostth1  26790  ostth3  26795  tgbtwnne  26860  tgbtwndiff  26876  tgcolg  26924  tgbtwnconn1lem3  26944  legso  26969  tglineeltr  27001  tglineintmo  27012  tglineneq  27014  colline  27019  mirne  27037  miriso  27040  mirhl  27049  mirbtwnhl  27050  symquadlem  27059  krippenlem  27060  midexlem  27062  ragncol  27079  footexALT  27088  footexlem2  27090  colperp  27099  colperpexlem3  27102  mideulem2  27104  opphllem  27105  midex  27107  opptgdim2  27115  oppperpex  27123  hlpasch  27126  colopp  27139  lmieu  27154  trgcopy  27174  cgracol  27198  cgrg3col4  27223  axlowdimlem15  27333  axcontlem2  27342  axcontlem7  27347  1egrvtxdg0  27887  2pthnloop  28108  cyclnspth  28177  eupth2lem1  28591  eupth2lem2  28592  eupth2lem3lem6  28606  strlem6  30627  hstrlem6  30635  atssma  30749  chirredlem1  30761  snsssng  30869  xaddeq0  31085  xlt2addrd  31090  fzone1  31130  divnumden2  31141  submomnd  31345  pmtridf1o  31370  pmtridfv1  31371  pmtridfv2  31372  ornglmullt  31515  orngrmullt  31516  ofldchr  31522  suborng  31523  pidlnz  31580  lindssn  31582  0ringprmidl  31634  qsidomlem1  31637  mxidlprm  31649  krull  31652  lindsunlem  31714  1smat1  31763  submatminr1  31769  madjusmdetlem2  31787  zarcls1  31828  zarclsint  31831  zarclssn  31832  xrge0iifcnv  31892  xrge0iifcv  31893  xrge0iif1  31897  qqhval2lem  31940  qqhf  31945  qqhre  31979  esumrnmpt2  32045  esumcvgre  32068  inelpisys  32131  carsgclctunlem2  32295  ballotlemirc  32507  sgnmul  32518  sgn0bi  32523  signswlid  32547  repr0  32600  reprlt  32608  reprgt  32610  reprinfz1  32611  tgoldbachgtda  32650  tgoldbachgt  32652  bnj1523  33060  acycgr2v  33121  fmlaomn0  33361  fmlasucdisj  33370  fz0n  33705  dfrdg2  33780  frxp2  33800  frxp3  33806  nolesgn2ores  33884  nogesgn1ores  33886  nosep1o  33893  nosep2o  33894  nosepdmlem  33895  nosepssdm  33898  noresle  33909  nosupbnd1lem3  33922  nosupbnd1lem4  33923  nosupbnd1lem5  33924  nosupbnd1lem6  33925  nosupbnd2lem1  33927  noinfbnd1lem3  33937  noinfbnd1lem4  33938  noinfbnd1lem5  33939  noinfbnd1lem6  33940  noinfbnd2lem1  33942  dfrdg4  34262  broutsideof2  34433  outsidele  34443  rankeq1o  34482  ivthALT  34533  limsucncmpi  34643  topdifinffinlem  35527  icorempo  35531  finxpreclem2  35570  finxp1o  35572  finxpreclem6  35576  poimirlem9  35795  poimirlem11  35797  poimirlem12  35798  poimirlem25  35811  fdc  35912  heibor1lem  35976  heiborlem4  35981  heiborlem6  35983  2atm  37548  lhpocnle  38037  lhp2at0nle  38056  trlval3  38208  cdleme18c  38314  cdlemg17b  38683  cdlemg17i  38690  dia2dimlem2  39086  dia2dimlem3  39087  dihord6apre  39277  dihatlat  39355  dochshpsat  39475  lcfrlem9  39571  mapdhval2  39747  hdmap1val2  39821  hdmap14lem4a  39892  hdmap14lem6  39894  dvrelogpow2b  40083  aks4d1p1p4  40086  aks4d1p6  40096  sticksstones1  40109  sticksstones10  40118  sticksstones12a  40120  sticksstones12  40121  sticksstones22  40131  metakunt6  40137  metakunt7  40138  metakunt11  40142  metakunt12  40143  metakunt27  40158  metakunt28  40159  metakunt29  40160  metakunt30  40161  mhpind  40290  negn0nposznnd  40317  nn0rppwr  40340  rtprmirr  40354  prjspner1  40470  dffltz  40478  3cubeslem2  40514  jm2.26lem3  40830  kelac1  40895  nlimsuc  41055  clsk1indlem0  41658  finnzfsuppd  41827  scotteld  41871  sineq0ALT  42564  refsum2cnlem1  42587  disjxp1  42624  nelrnmpt  42641  disjf1  42727  disjrnmpt2  42733  disjinfi  42738  oddfl  42823  xrlttri5d  42829  supxrge  42884  nepnfltpnf  42888  nemnftgtmnft  42890  xrlexaddrp  42898  xrred  42911  supminfxr2  43016  icoiccdif  43069  qinioo  43080  ioonct  43082  fmul01lt1lem1  43132  climrec  43151  limcperiod  43176  reclimc  43201  limsupub  43252  liminflbuz2  43363  cncfiooicclem1  43441  cncfioobdlem  43444  fperdvper  43467  dvdivbd  43471  ditgeqiooicc  43508  itgsincmulx  43522  itgioocnicc  43525  iblcncfioo  43526  stoweidlem35  43583  stoweidlem39  43587  stirlinglem5  43626  stirlinglem8  43629  dirkerper  43644  dirkercncflem2  43652  dirkercncflem4  43654  fourierdlem31  43686  fourierdlem34  43689  fourierdlem41  43696  fourierdlem42  43697  fourierdlem44  43699  fourierdlem48  43702  fourierdlem49  43703  fourierdlem53  43707  fourierdlem56  43710  fourierdlem58  43712  fourierdlem60  43714  fourierdlem61  43715  fourierdlem62  43716  fourierdlem65  43719  fourierdlem66  43720  fourierdlem73  43727  fourierdlem76  43730  fourierdlem79  43733  fourierdlem81  43735  fourierdlem82  43736  fourierdlem93  43747  fourierdlem103  43757  fourierdlem104  43758  sqwvfoura  43776  fourierswlem  43778  elaa2lem  43781  elaa2  43782  etransclem4  43786  etransclem24  43806  etransclem31  43813  etransclem32  43814  etransclem35  43817  sge0repnf  43931  sge0fodjrnlem  43961  sge0iunmpt  43963  sge0rpcpnf  43966  nnfoctbdjlem  44000  meadjun  44007  voliunsge0lem  44017  hoicvr  44093  ovnn0val  44096  ovnsubaddlem1  44115  hoidmvn0val  44129  hsphoidmvle  44131  hoidmv1lelem1  44136  hoidmv1lelem2  44137  hoidmv1lelem3  44138  ovnhoilem1  44146  ovnsubadd2lem  44190  ovnovollem3  44203  lighneallem3  45070  divgcdoddALTV  45145  dignn0flhalflem1  45972  itcoval2  46021  itcoval3  46022  itcovalsuc  46024  ackvalsuc1mpt  46035  line2xlem  46110