Theorem neneqd 2946

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

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 2942

This theorem is referenced by:  neneq  2947  necon2bi  2972  necon2i  2976  necon4i  2977  pm2.21ddne  3027  mteqand  3034  nelrdva  3702  eldifsnneq  4795  disjprg  5145  0inp0  5358  rnmptn0  6244  frxp2  8130  frxp3  8137  onnseq  8344  sniffsupp  9395  dfac2b  10125  ackbij1lem15  10229  ttukeylem7  10510  fpwwe2lem12  10637  canthnumlem  10643  canthp1lem2  10648  recgt0  12060  nnneneg  12247  elnnz  12568  xrnemnf  13097  xrnepnf  13098  fzprval  13562  fzodisjsn  13670  expnnval  14030  znsqcld  14127  hashelne0d  14328  elprchashprn2  14356  relexpsucnnr  14972  relexp1g  14973  relexpuzrel  14999  sgnp  15037  fprodn0f  15935  ruclem12  16184  dvdsle  16253  nndvdslegcd  16446  gcdnncl  16448  divgcdnn  16456  sqgcd  16502  eucalgf  16520  eucalginv  16521  lcmgcdlem  16543  lcmftp  16573  lcmfunsnlem2lem1  16575  lcmfunsnlem2lem2  16576  qredeu  16595  rpdvds  16597  cncongr2  16605  divnumden  16684  divdenle  16685  phisum  16723  oddprm  16743  pythagtriplem4  16752  pythagtriplem8  16756  pythagtriplem9  16757  4sqlem10  16880  ram0  16955  cat1lem  18046  isipodrs  18490  gsumval2  18605  smndex1n0mnd  18793  smndex2dnrinv  18796  mulgnn  18958  sylow1lem1  19466  gsumval3eu  19772  ablsimpgfindlem1  19977  ablsimpgfindlem2  19978  ablsimpgfind  19980  fincygsubgodd  19982  abvtrivd  20448  00lss  20552  lvecvscan2  20725  fidomndrng  20926  prmirredlem  21042  uvcff  21346  mvrcl  21551  mplmon  21590  mplmonmul  21591  coe1tmfv2  21797  cply1coe0  21823  cply1coe0bi  21824  1marepvsma1  22085  mdetrsca2  22106  mdetrlin2  22109  mdetunilem2  22115  mdetunilem5  22118  mdetunilem6  22119  mdetunilem9  22122  maducoeval2  22142  gsummatr01lem3  22159  gsummatr01lem4  22160  gsummatr01  22161  m2cpm  22243  m2cpminvid2lem  22256  fvmptnn04ifa  22352  fvmptnn04ifb  22353  fvmptnn04ifc  22354  chfacffsupp  22358  chfacfscmul0  22360  chfacfscmulgsum  22362  chfacfpmmul0  22364  chfacfpmmulgsum  22366  connclo  22919  dissnlocfin  23033  ptpjpre2  23084  txindis  23138  snfil  23368  alexsublem  23548  tsmsfbas  23632  stdbdxmet  24024  dscmet  24081  xrsxmet  24325  iccpnfcnv  24460  cphsubrglem  24694  minveclem3b  24945  minveclem4a  24947  ovolicc1  25033  dvexp2  25471  dvmptdiv  25491  lhop2  25532  deg1sublt  25628  ig1pval3  25692  dvply1  25797  plydiveu  25811  quotcan  25822  aaliou3lem9  25863  taylthlem2  25886  pserdvlem2  25940  abelthlem9  25952  logccne0  26087  logtayllem  26167  logtayl  26168  cxpef  26173  angrtmuld  26313  isosctrlem3  26325  chordthmlem  26337  leibpilem2  26446  leibpi  26447  rlimcnp2  26471  efrlim  26474  vma1  26670  muinv  26697  lgsval2lem  26810  lgsval4  26820  lgsdir  26835  lgseisenlem4  26881  lgsquadlem1  26883  lgsquad2  26889  m1lgs  26891  2sqlem8a  26928  2sqlem8  26929  2sqcoprm  26938  2sqmod  26939  padicabv  27133  ostth1  27136  ostth3  27141  nolesgn2ores  27175  nogesgn1ores  27177  nosep1o  27184  nosep2o  27185  nosepdmlem  27186  nosepssdm  27189  noresle  27200  nosupbnd1lem3  27213  nosupbnd1lem4  27214  nosupbnd1lem5  27215  nosupbnd1lem6  27216  nosupbnd2lem1  27218  noinfbnd1lem3  27228  noinfbnd1lem4  27229  noinfbnd1lem5  27230  noinfbnd1lem6  27231  noinfbnd2lem1  27233  0elold  27404  tgbtwnne  27772  tgbtwndiff  27788  tgcolg  27836  tgbtwnconn1lem3  27856  legso  27881  tglineeltr  27913  tglineintmo  27924  tglineneq  27926  colline  27931  mirne  27949  miriso  27952  mirhl  27961  mirbtwnhl  27962  symquadlem  27971  krippenlem  27972  midexlem  27974  ragncol  27991  footexALT  28000  footexlem2  28002  colperp  28011  colperpexlem3  28014  mideulem2  28016  opphllem  28017  midex  28019  opptgdim2  28027  oppperpex  28035  hlpasch  28038  colopp  28051  lmieu  28066  trgcopy  28086  cgracol  28110  cgrg3col4  28135  axlowdimlem15  28245  axcontlem2  28254  axcontlem7  28259  1egrvtxdg0  28799  2pthnloop  29019  cyclnspth  29088  eupth2lem1  29502  eupth2lem2  29503  eupth2lem3lem6  29517  nrt2irr  29757  strlem6  31540  hstrlem6  31548  atssma  31662  chirredlem1  31674  snsssng  31783  ifnetrue  31810  ifnefals  31811  xaddeq0  31997  xlt2addrd  32002  fzone1  32042  divnumden2  32055  submomnd  32259  pmtridf1o  32284  pmtridfv1  32285  pmtridfv2  32286  ornglmullt  32456  orngrmullt  32457  ofldchr  32463  suborng  32464  pidlnz  32519  lindssn  32525  drngidl  32582  drngidlhash  32583  0ringprmidl  32599  qsidomlem1  32602  mxidlmaxv  32615  mxidlprm  32617  mxidlirredi  32618  mxidlirred  32619  krull  32625  0ringmon1p  32667  ig1pnunit  32701  lindsunlem  32740  ply1annnr  32795  1smat1  32815  submatminr1  32821  madjusmdetlem2  32839  zarcls1  32880  zarclsint  32883  zarclssn  32884  xrge0iifcnv  32944  xrge0iifcv  32945  xrge0iif1  32949  qqhval2lem  32992  qqhf  32997  qqhre  33031  esumrnmpt2  33097  esumcvgre  33120  inelpisys  33183  carsgclctunlem2  33349  ballotlemirc  33561  sgnmul  33572  sgn0bi  33577  signswlid  33601  repr0  33654  reprlt  33662  reprgt  33664  reprinfz1  33665  tgoldbachgtda  33704  tgoldbachgt  33706  bnj1523  34113  acycgr2v  34172  fmlaomn0  34412  fmlasucdisj  34421  fz0n  34731  dfrdg2  34798  dfrdg4  34954  broutsideof2  35125  outsidele  35135  rankeq1o  35174  ivthALT  35268  limsucncmpi  35378  topdifinffinlem  36276  icorempo  36280  finxpreclem2  36319  finxp1o  36321  finxpreclem6  36325  poimirlem9  36545  poimirlem11  36547  poimirlem12  36548  poimirlem25  36561  fdc  36661  heibor1lem  36725  heiborlem4  36730  heiborlem6  36732  disjressuc2  37306  2atm  38446  lhpocnle  38935  lhp2at0nle  38954  trlval3  39106  cdleme18c  39212  cdlemg17b  39581  cdlemg17i  39588  dia2dimlem2  39984  dia2dimlem3  39985  dihord6apre  40175  dihatlat  40253  dochshpsat  40373  lcfrlem9  40469  mapdhval2  40645  hdmap1val2  40719  hdmap14lem4a  40790  hdmap14lem6  40792  dvrelogpow2b  40981  aks4d1p1p4  40984  aks4d1p6  40994  fldhmf1  41003  aks6d1c2p2  41005  sticksstones1  41010  sticksstones10  41019  sticksstones12a  41021  sticksstones12  41022  sticksstones22  41032  metakunt6  41038  metakunt7  41039  metakunt11  41043  metakunt12  41044  metakunt27  41059  metakunt28  41060  metakunt29  41061  metakunt30  41062  mhpind  41214  negn0nposznnd  41242  nn0rppwr  41272  rtprmirr  41285  prjspner1  41416  dffltz  41424  3cubeslem2  41471  jm2.26lem3  41788  kelac1  41853  cantnfresb  42122  tfsconcat0b  42144  nlimsuc  42240  clsk1indlem0  42840  finnzfsuppd  43009  scotteld  43053  sineq0ALT  43746  refsum2cnlem1  43769  disjxp1  43804  nelrnmpt  43821  disjf1  43928  disjrnmpt2  43934  disjinfi  43939  oddfl  44035  xrlttri5d  44041  supxrge  44096  nepnfltpnf  44100  nemnftgtmnft  44102  xrlexaddrp  44110  xrred  44123  supminfxr2  44227  icoiccdif  44285  qinioo  44296  ioonct  44298  fmul01lt1lem1  44348  climrec  44367  limcperiod  44392  reclimc  44417  limsupub  44468  liminflbuz2  44579  cncfiooicclem1  44657  cncfioobdlem  44660  fperdvper  44683  dvdivbd  44687  ditgeqiooicc  44724  itgsincmulx  44738  itgioocnicc  44741  iblcncfioo  44742  stoweidlem35  44799  stoweidlem39  44803  stirlinglem5  44842  stirlinglem8  44845  dirkerper  44860  dirkercncflem2  44868  dirkercncflem4  44870  fourierdlem31  44902  fourierdlem34  44905  fourierdlem41  44912  fourierdlem42  44913  fourierdlem44  44915  fourierdlem48  44918  fourierdlem49  44919  fourierdlem53  44923  fourierdlem56  44926  fourierdlem58  44928  fourierdlem60  44930  fourierdlem61  44931  fourierdlem62  44932  fourierdlem65  44935  fourierdlem66  44936  fourierdlem73  44943  fourierdlem76  44946  fourierdlem79  44949  fourierdlem81  44951  fourierdlem82  44952  fourierdlem93  44963  fourierdlem103  44973  fourierdlem104  44974  sqwvfoura  44992  fourierswlem  44994  elaa2lem  44997  elaa2  44998  etransclem4  45002  etransclem24  45022  etransclem31  45029  etransclem32  45030  etransclem35  45033  sge0repnf  45150  sge0fodjrnlem  45180  sge0iunmpt  45182  sge0rpcpnf  45185  nnfoctbdjlem  45219  meadjun  45226  voliunsge0lem  45236  hoicvr  45312  ovnn0val  45315  ovnsubaddlem1  45334  hoidmvn0val  45348  hsphoidmvle  45350  hoidmv1lelem1  45355  hoidmv1lelem2  45356  hoidmv1lelem3  45357  ovnhoilem1  45365  ovnsubadd2lem  45409  ovnovollem3  45422  lighneallem3  46323  divgcdoddALTV  46398  dignn0flhalflem1  47349  itcoval2  47398  itcoval3  47399  itcovalsuc  47401  ackvalsuc1mpt  47412  line2xlem  47487