Theorem neneqd 2947

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

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

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 2943

This theorem is referenced by:  neneq  2948  necon2bi  2973  necon2i  2977  necon4i  2978  pm2.21ddne  3028  mteqand  3047  nelrdva  3635  eldifsnneq  4721  disjprg  5066  0inp0  5276  rnmptn0  6136  onnseq  8146  sniffsupp  9089  dfac2b  9817  ackbij1lem15  9921  ttukeylem7  10202  fpwwe2lem12  10329  canthnumlem  10335  canthp1lem2  10340  recgt0  11751  nnneneg  11938  elnnz  12259  xrnemnf  12782  xrnepnf  12783  fzprval  13246  fzodisjsn  13353  expnnval  13713  znsqcld  13808  hashelne0d  14011  elprchashprn2  14039  relexpsucnnr  14664  relexp1g  14665  relexpuzrel  14691  sgnp  14729  fprodn0f  15629  ruclem12  15878  dvdsle  15947  nndvdslegcd  16140  gcdnncl  16142  divgcdnn  16150  sqgcd  16198  eucalgf  16216  eucalginv  16217  lcmgcdlem  16239  lcmftp  16269  lcmfunsnlem2lem1  16271  lcmfunsnlem2lem2  16272  qredeu  16291  rpdvds  16293  cncongr2  16301  divnumden  16380  divdenle  16381  phisum  16419  oddprm  16439  pythagtriplem4  16448  pythagtriplem8  16452  pythagtriplem9  16453  4sqlem10  16576  ram0  16651  cat1lem  17727  isipodrs  18170  gsumval2  18285  smndex1n0mnd  18466  smndex2dnrinv  18469  mulgnn  18623  sylow1lem1  19118  gsumval3eu  19420  ablsimpgfindlem1  19625  ablsimpgfindlem2  19626  ablsimpgfind  19628  fincygsubgodd  19630  abvtrivd  20015  00lss  20118  lvecvscan2  20289  fidomndrng  20492  prmirredlem  20606  uvcff  20908  mvrcl  21131  mplmon  21146  mplmonmul  21147  coe1tmfv2  21356  cply1coe0  21380  cply1coe0bi  21381  1marepvsma1  21640  mdetrsca2  21661  mdetrlin2  21664  mdetunilem2  21670  mdetunilem5  21673  mdetunilem6  21674  mdetunilem9  21677  maducoeval2  21697  gsummatr01lem3  21714  gsummatr01lem4  21715  gsummatr01  21716  m2cpm  21798  m2cpminvid2lem  21811  fvmptnn04ifa  21907  fvmptnn04ifb  21908  fvmptnn04ifc  21909  chfacffsupp  21913  chfacfscmul0  21915  chfacfscmulgsum  21917  chfacfpmmul0  21919  chfacfpmmulgsum  21921  connclo  22474  dissnlocfin  22588  ptpjpre2  22639  txindis  22693  snfil  22923  alexsublem  23103  tsmsfbas  23187  stdbdxmet  23577  dscmet  23634  xrsxmet  23878  iccpnfcnv  24013  cphsubrglem  24246  minveclem3b  24497  minveclem4a  24499  ovolicc1  24585  dvexp2  25023  dvmptdiv  25043  lhop2  25084  deg1sublt  25180  ig1pval3  25244  dvply1  25349  plydiveu  25363  quotcan  25374  aaliou3lem9  25415  taylthlem2  25438  pserdvlem2  25492  abelthlem9  25504  logccne0  25639  logtayllem  25719  logtayl  25720  cxpef  25725  angrtmuld  25863  isosctrlem3  25875  chordthmlem  25887  leibpilem2  25996  leibpi  25997  rlimcnp2  26021  efrlim  26024  vma1  26220  muinv  26247  lgsval2lem  26360  lgsval4  26370  lgsdir  26385  lgseisenlem4  26431  lgsquadlem1  26433  lgsquad2  26439  m1lgs  26441  2sqlem8a  26478  2sqlem8  26479  2sqcoprm  26488  2sqmod  26489  padicabv  26683  ostth1  26686  ostth3  26691  tgbtwnne  26755  tgbtwndiff  26771  tgcolg  26819  tgbtwnconn1lem3  26839  legso  26864  tglineeltr  26896  tglineintmo  26907  tglineneq  26909  colline  26914  mirne  26932  miriso  26935  mirhl  26944  mirbtwnhl  26945  symquadlem  26954  krippenlem  26955  midexlem  26957  ragncol  26974  footexALT  26983  footexlem2  26985  colperp  26994  colperpexlem3  26997  mideulem2  26999  opphllem  27000  midex  27002  opptgdim2  27010  oppperpex  27018  hlpasch  27021  colopp  27034  lmieu  27049  trgcopy  27069  cgracol  27093  cgrg3col4  27118  axlowdimlem15  27227  axcontlem2  27236  axcontlem7  27241  1egrvtxdg0  27781  2pthnloop  28000  cyclnspth  28069  eupth2lem1  28483  eupth2lem2  28484  eupth2lem3lem6  28498  strlem6  30519  hstrlem6  30527  atssma  30641  chirredlem1  30653  snsssng  30761  xaddeq0  30978  xlt2addrd  30983  fzone1  31023  divnumden2  31034  submomnd  31238  pmtridf1o  31263  pmtridfv1  31264  pmtridfv2  31265  ornglmullt  31408  orngrmullt  31409  ofldchr  31415  suborng  31416  pidlnz  31473  lindssn  31475  0ringprmidl  31527  qsidomlem1  31530  mxidlprm  31542  krull  31545  lindsunlem  31607  1smat1  31656  submatminr1  31662  madjusmdetlem2  31680  zarcls1  31721  zarclsint  31724  zarclssn  31725  xrge0iifcnv  31785  xrge0iifcv  31786  xrge0iif1  31790  qqhval2lem  31831  qqhf  31836  qqhre  31870  esumrnmpt2  31936  esumcvgre  31959  inelpisys  32022  carsgclctunlem2  32186  ballotlemirc  32398  sgnmul  32409  sgn0bi  32414  signswlid  32438  repr0  32491  reprlt  32499  reprgt  32501  reprinfz1  32502  tgoldbachgtda  32541  tgoldbachgt  32543  bnj1523  32951  acycgr2v  33012  fmlaomn0  33252  fmlasucdisj  33261  fz0n  33602  dfrdg2  33677  frxp2  33718  frxp3  33724  nolesgn2ores  33802  nogesgn1ores  33804  nosep1o  33811  nosep2o  33812  nosepdmlem  33813  nosepssdm  33816  noresle  33827  nosupbnd1lem3  33840  nosupbnd1lem4  33841  nosupbnd1lem5  33842  nosupbnd1lem6  33843  nosupbnd2lem1  33845  noinfbnd1lem3  33855  noinfbnd1lem4  33856  noinfbnd1lem5  33857  noinfbnd1lem6  33858  noinfbnd2lem1  33860  dfrdg4  34180  broutsideof2  34351  outsidele  34361  rankeq1o  34400  ivthALT  34451  limsucncmpi  34561  topdifinffinlem  35445  icorempo  35449  finxpreclem2  35488  finxp1o  35490  finxpreclem6  35494  poimirlem9  35713  poimirlem11  35715  poimirlem12  35716  poimirlem25  35729  fdc  35830  heibor1lem  35894  heiborlem4  35899  heiborlem6  35901  2atm  37468  lhpocnle  37957  lhp2at0nle  37976  trlval3  38128  cdleme18c  38234  cdlemg17b  38603  cdlemg17i  38610  dia2dimlem2  39006  dia2dimlem3  39007  dihord6apre  39197  dihatlat  39275  dochshpsat  39395  lcfrlem9  39491  mapdhval2  39667  hdmap1val2  39741  hdmap14lem4a  39812  hdmap14lem6  39814  dvrelogpow2b  40004  aks4d1p1p4  40007  aks4d1p6  40017  sticksstones1  40030  sticksstones10  40039  sticksstones12a  40041  sticksstones12  40042  sticksstones22  40052  metakunt6  40058  metakunt7  40059  metakunt11  40063  metakunt12  40064  metakunt27  40079  metakunt28  40080  metakunt29  40081  metakunt30  40082  mhpind  40206  negn0nposznnd  40231  nn0rppwr  40254  rtprmirr  40268  prjspner1  40384  dffltz  40387  3cubeslem2  40423  jm2.26lem3  40739  kelac1  40804  clsk1indlem0  41540  finnzfsuppd  41709  scotteld  41753  sineq0ALT  42446  refsum2cnlem1  42469  disjxp1  42506  nelrnmpt  42523  disjf1  42609  disjrnmpt2  42615  disjinfi  42620  oddfl  42705  xrlttri5d  42711  supxrge  42767  nepnfltpnf  42771  nemnftgtmnft  42773  xrlexaddrp  42781  xrred  42794  supminfxr2  42899  icoiccdif  42952  qinioo  42963  ioonct  42965  fmul01lt1lem1  43015  climrec  43034  limcperiod  43059  reclimc  43084  limsupub  43135  liminflbuz2  43246  cncfiooicclem1  43324  cncfioobdlem  43327  fperdvper  43350  dvdivbd  43354  ditgeqiooicc  43391  itgsincmulx  43405  itgioocnicc  43408  iblcncfioo  43409  stoweidlem35  43466  stoweidlem39  43470  stirlinglem5  43509  stirlinglem8  43512  dirkerper  43527  dirkercncflem2  43535  dirkercncflem4  43537  fourierdlem31  43569  fourierdlem34  43572  fourierdlem41  43579  fourierdlem42  43580  fourierdlem44  43582  fourierdlem48  43585  fourierdlem49  43586  fourierdlem53  43590  fourierdlem56  43593  fourierdlem58  43595  fourierdlem60  43597  fourierdlem61  43598  fourierdlem62  43599  fourierdlem65  43602  fourierdlem66  43603  fourierdlem73  43610  fourierdlem76  43613  fourierdlem79  43616  fourierdlem81  43618  fourierdlem82  43619  fourierdlem93  43630  fourierdlem103  43640  fourierdlem104  43641  sqwvfoura  43659  fourierswlem  43661  elaa2lem  43664  elaa2  43665  etransclem4  43669  etransclem24  43689  etransclem31  43696  etransclem32  43697  etransclem35  43700  sge0repnf  43814  sge0fodjrnlem  43844  sge0iunmpt  43846  sge0rpcpnf  43849  nnfoctbdjlem  43883  meadjun  43890  voliunsge0lem  43900  hoicvr  43976  ovnn0val  43979  ovnsubaddlem1  43998  hoidmvn0val  44012  hsphoidmvle  44014  hoidmv1lelem1  44019  hoidmv1lelem2  44020  hoidmv1lelem3  44021  ovnhoilem1  44029  ovnsubadd2lem  44073  ovnovollem3  44086  lighneallem3  44947  divgcdoddALTV  45022  dignn0flhalflem1  45849  itcoval2  45898  itcoval3  45899  itcovalsuc  45901  ackvalsuc1mpt  45912  line2xlem  45987