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  3676  eldifsnneq  4755  disjprg  5103  0inp0  5314  rnmptn0  6217  resf1extb  7910  frxp2  8123  frxp3  8130  onnseq  8313  finnzfsuppd  9324  sniffsupp  9351  dfac2b  10084  ackbij1lem15  10186  ttukeylem7  10468  fpwwe2lem12  10595  canthnumlem  10601  canthp1lem2  10606  recgt0  12028  nnneneg  12221  elnnz  12539  xrnemnf  13077  xrnepnf  13078  fzprval  13546  fzodisjsn  13658  expnnval  14029  znsqcld  14127  hashelne0d  14333  elprchashprn2  14361  relexpsucnnr  14991  relexp1g  14992  relexpuzrel  15018  sgnp  15056  fprodn0f  15957  ruclem12  16209  dvdsle  16280  nndvdslegcd  16475  gcdnncl  16477  divgcdnn  16485  nn0rppwr  16531  sqgcd  16532  eucalgf  16553  eucalginv  16554  lcmgcdlem  16576  lcmftp  16606  lcmfunsnlem2lem1  16608  lcmfunsnlem2lem2  16609  qredeu  16628  rpdvds  16630  cncongr2  16638  divnumden  16718  divdenle  16719  phisum  16761  oddprm  16781  pythagtriplem4  16790  pythagtriplem8  16794  pythagtriplem9  16795  4sqlem10  16918  ram0  16993  cat1lem  18058  isipodrs  18496  gsumval2  18613  smndex1n0mnd  18839  smndex2dnrinv  18842  mulgnn  19007  sylow1lem1  19528  gsumval3eu  19834  ablsimpgfindlem1  20039  ablsimpgfindlem2  20040  ablsimpgfind  20042  fincygsubgodd  20044  rrgnz  20613  fidomndrng  20682  abvtrivd  20741  00lss  20847  lvecvscan2  21022  prmirredlem  21382  uvcff  21700  mvrcl  21901  mplmon  21942  mplmonmul  21943  psdmul  22053  coe1tmfv2  22161  cply1coe0  22188  cply1coe0bi  22189  1marepvsma1  22470  mdetrsca2  22491  mdetrlin2  22494  mdetunilem2  22500  mdetunilem5  22503  mdetunilem6  22504  mdetunilem9  22507  maducoeval2  22527  gsummatr01lem3  22544  gsummatr01lem4  22545  gsummatr01  22546  m2cpm  22628  m2cpminvid2lem  22641  fvmptnn04ifa  22737  fvmptnn04ifb  22738  fvmptnn04ifc  22739  chfacffsupp  22743  chfacfscmul0  22745  chfacfscmulgsum  22747  chfacfpmmul0  22749  chfacfpmmulgsum  22751  connclo  23302  dissnlocfin  23416  ptpjpre2  23467  txindis  23521  snfil  23751  alexsublem  23931  tsmsfbas  24015  stdbdxmet  24403  dscmet  24460  xrsxmet  24698  iccpnfcnv  24842  cphsubrglem  25077  minveclem3b  25328  minveclem4a  25330  ovolicc1  25417  dvexp2  25858  dvmptdiv  25878  lhop2  25920  deg1sublt  26015  ig1pval3  26083  dvply1  26191  plydiveu  26206  quotcan  26217  aaliou3lem9  26258  taylthlem2  26282  taylthlem2OLD  26283  pserdvlem2  26338  abelthlem9  26350  logccne0  26487  logtayllem  26568  logtayl  26569  cxpef  26574  rtprmirr  26670  angrtmuld  26718  isosctrlem3  26730  chordthmlem  26742  leibpilem2  26851  leibpi  26852  rlimcnp2  26876  efrlim  26879  efrlimOLD  26880  vma1  27076  muinv  27103  lgsval2lem  27218  lgsval4  27228  lgsdir  27243  lgseisenlem4  27289  lgsquadlem1  27291  lgsquad2  27297  m1lgs  27299  2sqlem8a  27336  2sqlem8  27337  2sqcoprm  27346  2sqmod  27347  padicabv  27541  ostth1  27544  ostth3  27549  nolesgn2ores  27584  nogesgn1ores  27586  nosep1o  27593  nosep2o  27594  nosepdmlem  27595  nosepssdm  27598  noresle  27609  nosupbnd1lem3  27622  nosupbnd1lem4  27623  nosupbnd1lem5  27624  nosupbnd1lem6  27625  nosupbnd2lem1  27627  noinfbnd1lem3  27637  noinfbnd1lem4  27638  noinfbnd1lem5  27639  noinfbnd1lem6  27640  noinfbnd2lem1  27642  0elold  27821  elnnzs  28289  expsnnval  28312  expsne0  28321  tgbtwnne  28417  tgbtwndiff  28433  tgcolg  28481  tgbtwnconn1lem3  28501  legso  28526  tglineeltr  28558  tglineintmo  28569  tglineneq  28571  colline  28576  mirne  28594  miriso  28597  mirhl  28606  mirbtwnhl  28607  symquadlem  28616  krippenlem  28617  midexlem  28619  ragncol  28636  footexALT  28645  footexlem2  28647  colperp  28656  colperpexlem3  28659  mideulem2  28661  opphllem  28662  midex  28664  opptgdim2  28672  oppperpex  28680  hlpasch  28683  colopp  28696  lmieu  28711  trgcopy  28731  cgracol  28755  cgrg3col4  28780  axlowdimlem15  28883  axcontlem2  28892  axcontlem7  28897  1egrvtxdg0  29439  2pthnloop  29661  cyclnspth  29731  eupth2lem1  30147  eupth2lem2  30148  eupth2lem3lem6  30162  nrt2irr  30402  strlem6  32185  hstrlem6  32193  atssma  32307  chirredlem1  32319  snsssng  32443  ifnetrue  32476  ifnefals  32477  fmptunsnop  32623  xaddeq0  32676  rexmul2  32677  xlt2addrd  32682  xnn0nn0d  32695  fzone1  32723  hashpss  32734  elq2  32736  divnumden2  32740  sgnmul  32760  sgn0bi  32765  2exple2exp  32770  chnub  32938  submomnd  33024  pmtridf1o  33051  pmtridfv1  33052  pmtridfv2  33053  elrgspnlem2  33194  elrgspnlem3  33195  fracfld  33258  ornglmullt  33285  orngrmullt  33286  ofldchr  33292  suborng  33293  pidlnz  33347  lindssn  33349  drngidl  33404  drngidlhash  33405  0ringprmidl  33420  qsidomlem1  33423  ssdifidlprm  33429  mxidlmaxv  33439  mxidlprm  33441  mxidlirredi  33442  mxidlirred  33443  krull  33450  rsprprmprmidlb  33494  rprmasso2  33497  pidufd  33514  1arithufdlem3  33517  dfufd2  33521  zringidom  33522  0ringmon1p  33526  ig1pnunit  33566  lindsunlem  33620  fldextrspundgdvdslem  33675  fldext2rspun  33677  ply1annnr  33693  fldext2chn  33718  constrextdg2lem  33738  constrext2chnlem  33740  constrcon  33764  2sqr3minply  33770  cos9thpiminply  33778  1smat1  33794  submatminr1  33800  madjusmdetlem2  33818  zarcls1  33859  zarclsint  33862  zarclssn  33863  xrge0iifcnv  33923  xrge0iifcv  33924  xrge0iif1  33928  qqhval2lem  33971  qqhf  33976  qqhre  34010  esumrnmpt2  34058  esumcvgre  34081  inelpisys  34144  carsgclctunlem2  34310  ballotlemirc  34523  signswlid  34550  repr0  34602  reprlt  34610  reprgt  34612  reprinfz1  34613  tgoldbachgtda  34652  tgoldbachgt  34654  bnj1523  35061  acycgr2v  35137  fmlaomn0  35377  fmlasucdisj  35386  fz0n  35718  dfrdg2  35783  dfrdg4  35939  broutsideof2  36110  outsidele  36120  rankeq1o  36159  ivthALT  36323  limsucncmpi  36433  topdifinffinlem  37335  icorempo  37339  finxpreclem2  37378  finxp1o  37380  finxpreclem6  37384  poimirlem9  37623  poimirlem11  37625  poimirlem12  37626  poimirlem25  37639  fdc  37739  heibor1lem  37803  heiborlem4  37808  heiborlem6  37810  disjressuc2  38374  2atm  39521  lhpocnle  40010  lhp2at0nle  40029  trlval3  40181  cdleme18c  40287  cdlemg17b  40656  cdlemg17i  40663  dia2dimlem2  41059  dia2dimlem3  41060  dihord6apre  41250  dihatlat  41328  dochshpsat  41448  lcfrlem9  41544  mapdhval2  41720  hdmap1val2  41794  hdmap14lem4a  41865  hdmap14lem6  41867  dvrelogpow2b  42056  aks4d1p1p4  42059  aks4d1p6  42069  fldhmf1  42078  primrootspoweq0  42094  aks6d1c2p2  42107  hashscontpow  42110  aks6d1c5  42127  sticksstones1  42134  sticksstones10  42143  sticksstones12a  42145  sticksstones12  42146  sticksstones22  42156  aks6d1c6lem4  42161  aks6d1c7lem1  42168  aks6d1c7  42172  aks5lem8  42189  negn0nposznnd  42270  mhpind  42582  prjspner1  42614  dffltz  42622  3cubeslem2  42673  jm2.26lem3  42990  kelac1  43052  cantnfresb  43313  tfsconcat0b  43335  nlimsuc  43430  clsk1indlem0  44030  scotteld  44235  sineq0ALT  44926  refsum2cnlem1  45031  disjxp1  45063  nelrnmpt  45078  disjf1  45177  disjrnmpt2  45182  disjinfi  45186  oddfl  45276  xrlttri5d  45282  supxrge  45334  nepnfltpnf  45338  nemnftgtmnft  45340  xrlexaddrp  45348  xrred  45361  supminfxr2  45465  icoiccdif  45522  qinioo  45533  ioonct  45535  fmul01lt1lem1  45582  climrec  45601  limcperiod  45626  reclimc  45651  limsupub  45702  liminflbuz2  45813  cncfiooicclem1  45891  cncfioobdlem  45894  fperdvper  45917  dvdivbd  45921  ditgeqiooicc  45958  itgsincmulx  45972  itgioocnicc  45975  iblcncfioo  45976  stoweidlem35  46033  stoweidlem39  46037  stirlinglem5  46076  stirlinglem8  46079  dirkerper  46094  dirkercncflem2  46102  dirkercncflem4  46104  fourierdlem31  46136  fourierdlem34  46139  fourierdlem41  46146  fourierdlem42  46147  fourierdlem44  46149  fourierdlem48  46152  fourierdlem49  46153  fourierdlem53  46157  fourierdlem56  46160  fourierdlem58  46162  fourierdlem60  46164  fourierdlem61  46165  fourierdlem62  46166  fourierdlem65  46169  fourierdlem66  46170  fourierdlem73  46177  fourierdlem76  46180  fourierdlem79  46183  fourierdlem81  46185  fourierdlem82  46186  fourierdlem93  46197  fourierdlem103  46207  fourierdlem104  46208  sqwvfoura  46226  fourierswlem  46228  elaa2lem  46231  elaa2  46232  etransclem4  46236  etransclem24  46256  etransclem31  46263  etransclem32  46264  etransclem35  46267  sge0repnf  46384  sge0fodjrnlem  46414  sge0iunmpt  46416  sge0rpcpnf  46419  nnfoctbdjlem  46453  meadjun  46460  voliunsge0lem  46470  hoicvr  46546  ovnn0val  46549  ovnsubaddlem1  46568  hoidmvn0val  46582  hsphoidmvle  46584  hoidmv1lelem1  46589  hoidmv1lelem2  46590  hoidmv1lelem3  46591  ovnhoilem1  46599  ovnsubadd2lem  46643  ovnovollem3  46656  cjnpoly  46890  lighneallem3  47608  divgcdoddALTV  47683  isubgr0uhgr  47873  usgrexmpl2trifr  48028  gpg5nbgrvtx03star  48071  gpg5nbgr3star  48072  dignn0flhalflem1  48604  itcoval2  48653  itcoval3  48654  itcovalsuc  48656  ackvalsuc1mpt  48667  line2xlem  48742