Theorem neneqd 2935

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2930

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 2931

This theorem is referenced by:  neneq  2936  necon2bi  2960  necon2i  2964  necon4i  2965  pm2.21ddne  3014  mteqand  3021  nelrdva  3661  eldifsnneq  4745  disjprg  5092  0inp0  5302  nelrnmpt  5914  rnmptn0  6200  resf1extb  7874  frxp2  8084  frxp3  8091  onnseq  8274  finnzfsuppd  9274  sniffsupp  9301  dfac2b  10039  ackbij1lem15  10141  ttukeylem7  10423  fpwwe2lem12  10551  canthnumlem  10557  canthp1lem2  10562  recgt0  11985  nnneneg  12178  elnnz  12496  xrnemnf  13029  xrnepnf  13030  fzprval  13499  fzodisjsn  13611  fzone1  13698  expnnval  13985  znsqcld  14083  hashelne0d  14289  elprchashprn2  14317  relexpsucnnr  14946  relexp1g  14947  relexpuzrel  14973  sgnp  15011  fprodn0f  15912  ruclem12  16164  dvdsle  16235  nndvdslegcd  16430  gcdnncl  16432  divgcdnn  16440  nn0rppwr  16486  sqgcd  16487  eucalgf  16508  eucalginv  16509  lcmgcdlem  16531  lcmftp  16561  lcmfunsnlem2lem1  16563  lcmfunsnlem2lem2  16564  qredeu  16583  rpdvds  16585  cncongr2  16593  divnumden  16673  divdenle  16674  phisum  16716  oddprm  16736  pythagtriplem4  16745  pythagtriplem8  16749  pythagtriplem9  16750  4sqlem10  16873  ram0  16948  cat1lem  18018  isipodrs  18458  chnub  18543  chnpof1  18551  gsumval2  18609  smndex1n0mnd  18835  smndex2dnrinv  18838  mulgnn  19003  sylow1lem1  19525  gsumval3eu  19831  ablsimpgfindlem1  20036  ablsimpgfindlem2  20037  ablsimpgfind  20039  fincygsubgodd  20041  submomnd  20059  rrgnz  20635  fidomndrng  20704  abvtrivd  20763  ornglmullt  20800  orngrmullt  20801  suborng  20807  00lss  20890  lvecvscan2  21065  prmirredlem  21425  ofldchr  21529  uvcff  21744  mvrcl  21945  mplmon  21988  mplmonmul  21989  psdmul  22107  coe1tmfv2  22215  cply1coe0  22243  cply1coe0bi  22244  1marepvsma1  22525  mdetrsca2  22546  mdetrlin2  22549  mdetunilem2  22555  mdetunilem5  22558  mdetunilem6  22559  mdetunilem9  22562  maducoeval2  22582  gsummatr01lem3  22599  gsummatr01lem4  22600  gsummatr01  22601  m2cpm  22683  m2cpminvid2lem  22696  fvmptnn04ifa  22792  fvmptnn04ifb  22793  fvmptnn04ifc  22794  chfacffsupp  22798  chfacfscmul0  22800  chfacfscmulgsum  22802  chfacfpmmul0  22804  chfacfpmmulgsum  22806  connclo  23357  dissnlocfin  23471  ptpjpre2  23522  txindis  23576  snfil  23806  alexsublem  23986  tsmsfbas  24070  stdbdxmet  24457  dscmet  24514  xrsxmet  24752  iccpnfcnv  24896  cphsubrglem  25131  minveclem3b  25382  minveclem4a  25384  ovolicc1  25471  dvexp2  25912  dvmptdiv  25932  lhop2  25974  deg1sublt  26069  ig1pval3  26137  dvply1  26245  plydiveu  26260  quotcan  26271  aaliou3lem9  26312  taylthlem2  26336  taylthlem2OLD  26337  pserdvlem2  26392  abelthlem9  26404  logccne0  26541  logtayllem  26622  logtayl  26623  cxpef  26628  rtprmirr  26724  angrtmuld  26772  isosctrlem3  26784  chordthmlem  26796  leibpilem2  26905  leibpi  26906  rlimcnp2  26930  efrlim  26933  efrlimOLD  26934  vma1  27130  muinv  27157  lgsval2lem  27272  lgsval4  27282  lgsdir  27297  lgseisenlem4  27343  lgsquadlem1  27345  lgsquad2  27351  m1lgs  27353  2sqlem8a  27390  2sqlem8  27391  2sqcoprm  27400  2sqmod  27401  padicabv  27595  ostth1  27598  ostth3  27603  nolesgn2ores  27638  nogesgn1ores  27640  nosep1o  27647  nosep2o  27648  nosepdmlem  27649  nosepssdm  27652  noresle  27663  nosupbnd1lem3  27676  nosupbnd1lem4  27677  nosupbnd1lem5  27678  nosupbnd1lem6  27679  nosupbnd2lem1  27681  noinfbnd1lem3  27691  noinfbnd1lem4  27692  noinfbnd1lem5  27693  noinfbnd1lem6  27694  noinfbnd2lem1  27696  0elold  27882  elnnzs  28359  expsnnval  28384  expsne0  28394  tgbtwnne  28511  tgbtwndiff  28527  tgcolg  28575  tgbtwnconn1lem3  28595  legso  28620  tglineeltr  28652  tglineintmo  28663  tglineneq  28665  colline  28670  mirne  28688  miriso  28691  mirhl  28700  mirbtwnhl  28701  symquadlem  28710  krippenlem  28711  midexlem  28713  ragncol  28730  footexALT  28739  footexlem2  28741  colperp  28750  colperpexlem3  28753  mideulem2  28755  opphllem  28756  midex  28758  opptgdim2  28766  oppperpex  28774  hlpasch  28777  colopp  28790  lmieu  28805  trgcopy  28825  cgracol  28849  cgrg3col4  28874  axlowdimlem15  28978  axcontlem2  28987  axcontlem7  28992  1egrvtxdg0  29534  2pthnloop  29753  cyclnspth  29823  eupth2lem1  30242  eupth2lem2  30243  eupth2lem3lem6  30257  nrt2irr  30497  strlem6  32280  hstrlem6  32288  atssma  32402  chirredlem1  32414  snsssng  32538  ifnetrue  32571  ifnefals  32572  fmptunsnop  32728  xaddeq0  32782  rexmul2  32783  xlt2addrd  32788  xnn0nn0d  32801  hashpss  32838  elq2  32841  divnumden2  32845  sgnmul  32865  sgn0bi  32870  2exple2exp  32875  pmtridf1o  33125  pmtridfv1  33126  pmtridfv2  33127  elrgspnlem2  33274  elrgspnlem3  33275  domnprodeq0  33307  fracfld  33339  pidlnz  33406  lindssn  33408  drngidl  33463  drngidlhash  33464  0ringprmidl  33479  qsidomlem1  33482  ssdifidlprm  33488  mxidlmaxv  33498  mxidlprm  33500  mxidlirredi  33501  mxidlirred  33502  krull  33509  rsprprmprmidlb  33553  rprmasso2  33556  pidufd  33573  1arithufdlem3  33576  dfufd2  33580  zringidom  33581  0ringmon1p  33587  ig1pnunit  33631  mplmulmvr  33653  esplyfval2  33672  esplymhp  33675  esplyfval3  33679  vietadeg1  33683  lindsunlem  33730  fldextrspundgdvdslem  33786  fldext2rspun  33788  ply1annnr  33809  fldext2chn  33834  constrextdg2lem  33854  constrext2chnlem  33856  constrcon  33880  2sqr3minply  33886  cos9thpiminply  33894  1smat1  33910  submatminr1  33916  madjusmdetlem2  33934  zarcls1  33975  zarclsint  33978  zarclssn  33979  xrge0iifcnv  34039  xrge0iifcv  34040  xrge0iif1  34044  qqhval2lem  34087  qqhf  34092  qqhre  34126  esumrnmpt2  34174  esumcvgre  34197  inelpisys  34260  carsgclctunlem2  34425  ballotlemirc  34638  signswlid  34665  repr0  34717  reprlt  34725  reprgt  34727  reprinfz1  34728  tgoldbachgtda  34767  tgoldbachgt  34769  bnj1523  35176  acycgr2v  35293  fmlaomn0  35533  fmlasucdisj  35542  fz0n  35874  dfrdg2  35936  dfrdg4  36094  broutsideof2  36265  outsidele  36275  rankeq1o  36314  ivthALT  36478  limsucncmpi  36588  topdifinffinlem  37491  icorempo  37495  finxpreclem2  37534  finxp1o  37536  finxpreclem6  37540  poimirlem9  37769  poimirlem11  37771  poimirlem12  37772  poimirlem25  37785  fdc  37885  heibor1lem  37949  heiborlem4  37954  heiborlem6  37956  disjressuc2  38535  2atm  39726  lhpocnle  40215  lhp2at0nle  40234  trlval3  40386  cdleme18c  40492  cdlemg17b  40861  cdlemg17i  40868  dia2dimlem2  41264  dia2dimlem3  41265  dihord6apre  41455  dihatlat  41533  dochshpsat  41653  lcfrlem9  41749  mapdhval2  41925  hdmap1val2  41999  hdmap14lem4a  42070  hdmap14lem6  42072  dvrelogpow2b  42261  aks4d1p1p4  42264  aks4d1p6  42274  fldhmf1  42283  primrootspoweq0  42299  aks6d1c2p2  42312  hashscontpow  42315  aks6d1c5  42332  sticksstones1  42339  sticksstones10  42348  sticksstones12a  42350  sticksstones12  42351  sticksstones22  42361  aks6d1c6lem4  42366  aks6d1c7lem1  42373  aks6d1c7  42377  aks5lem8  42394  negn0nposznnd  42479  mhpind  42779  prjspner1  42811  dffltz  42819  3cubeslem2  42869  jm2.26lem3  43185  kelac1  43247  cantnfresb  43508  tfsconcat0b  43530  nlimsuc  43624  clsk1indlem0  44224  scotteld  44429  sineq0ALT  45119  refsum2cnlem1  45224  disjxp1  45256  disjf1  45369  disjrnmpt2  45374  disjinfi  45378  oddfl  45468  xrlttri5d  45474  supxrge  45525  nepnfltpnf  45529  nemnftgtmnft  45531  xrlexaddrp  45539  xrred  45551  supminfxr2  45655  icoiccdif  45712  qinioo  45723  ioonct  45725  fmul01lt1lem1  45772  climrec  45791  limcperiod  45816  reclimc  45839  limsupub  45890  liminflbuz2  46001  cncfiooicclem1  46079  cncfioobdlem  46082  fperdvper  46105  dvdivbd  46109  ditgeqiooicc  46146  itgsincmulx  46160  itgioocnicc  46163  iblcncfioo  46164  stoweidlem35  46221  stoweidlem39  46225  stirlinglem5  46264  stirlinglem8  46267  dirkerper  46282  dirkercncflem2  46290  dirkercncflem4  46292  fourierdlem31  46324  fourierdlem34  46327  fourierdlem41  46334  fourierdlem42  46335  fourierdlem44  46337  fourierdlem48  46340  fourierdlem49  46341  fourierdlem53  46345  fourierdlem56  46348  fourierdlem58  46350  fourierdlem60  46352  fourierdlem61  46353  fourierdlem62  46354  fourierdlem65  46357  fourierdlem66  46358  fourierdlem73  46365  fourierdlem76  46368  fourierdlem79  46371  fourierdlem81  46373  fourierdlem82  46374  fourierdlem93  46385  fourierdlem103  46395  fourierdlem104  46396  sqwvfoura  46414  fourierswlem  46416  elaa2lem  46419  elaa2  46420  etransclem4  46424  etransclem24  46444  etransclem31  46451  etransclem32  46452  etransclem35  46455  sge0repnf  46572  sge0fodjrnlem  46602  sge0iunmpt  46604  sge0rpcpnf  46607  nnfoctbdjlem  46641  meadjun  46648  voliunsge0lem  46658  hoicvr  46734  ovnn0val  46737  ovnsubaddlem1  46756  hoidmvn0val  46770  hsphoidmvle  46772  hoidmv1lelem1  46777  hoidmv1lelem2  46778  hoidmv1lelem3  46779  ovnhoilem1  46787  ovnsubadd2lem  46831  ovnovollem3  46844  cjnpoly  47077  lighneallem3  47795  divgcdoddALTV  47870  isubgr0uhgr  48061  usgrexmpl2trifr  48225  gpg5nbgrvtx03star  48268  gpg5nbgr3star  48269  dignn0flhalflem1  48803  itcoval2  48852  itcoval3  48853  itcovalsuc  48855  ackvalsuc1mpt  48866  line2xlem  48941