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  3673  eldifsnneq  4751  disjprg  5098  0inp0  5309  rnmptn0  6205  resf1extb  7890  frxp2  8100  frxp3  8107  onnseq  8290  finnzfsuppd  9300  sniffsupp  9327  dfac2b  10060  ackbij1lem15  10162  ttukeylem7  10444  fpwwe2lem12  10571  canthnumlem  10577  canthp1lem2  10582  recgt0  12004  nnneneg  12197  elnnz  12515  xrnemnf  13053  xrnepnf  13054  fzprval  13522  fzodisjsn  13634  expnnval  14005  znsqcld  14103  hashelne0d  14309  elprchashprn2  14337  relexpsucnnr  14967  relexp1g  14968  relexpuzrel  14994  sgnp  15032  fprodn0f  15933  ruclem12  16185  dvdsle  16256  nndvdslegcd  16451  gcdnncl  16453  divgcdnn  16461  nn0rppwr  16507  sqgcd  16508  eucalgf  16529  eucalginv  16530  lcmgcdlem  16552  lcmftp  16582  lcmfunsnlem2lem1  16584  lcmfunsnlem2lem2  16585  qredeu  16604  rpdvds  16606  cncongr2  16614  divnumden  16694  divdenle  16695  phisum  16737  oddprm  16757  pythagtriplem4  16766  pythagtriplem8  16770  pythagtriplem9  16771  4sqlem10  16894  ram0  16969  cat1lem  18038  isipodrs  18478  gsumval2  18595  smndex1n0mnd  18821  smndex2dnrinv  18824  mulgnn  18989  sylow1lem1  19512  gsumval3eu  19818  ablsimpgfindlem1  20023  ablsimpgfindlem2  20024  ablsimpgfind  20026  fincygsubgodd  20028  submomnd  20046  rrgnz  20624  fidomndrng  20693  abvtrivd  20752  ornglmullt  20789  orngrmullt  20790  suborng  20796  00lss  20879  lvecvscan2  21054  prmirredlem  21414  ofldchr  21518  uvcff  21733  mvrcl  21934  mplmon  21975  mplmonmul  21976  psdmul  22086  coe1tmfv2  22194  cply1coe0  22221  cply1coe0bi  22222  1marepvsma1  22503  mdetrsca2  22524  mdetrlin2  22527  mdetunilem2  22533  mdetunilem5  22536  mdetunilem6  22537  mdetunilem9  22540  maducoeval2  22560  gsummatr01lem3  22577  gsummatr01lem4  22578  gsummatr01  22579  m2cpm  22661  m2cpminvid2lem  22674  fvmptnn04ifa  22770  fvmptnn04ifb  22771  fvmptnn04ifc  22772  chfacffsupp  22776  chfacfscmul0  22778  chfacfscmulgsum  22780  chfacfpmmul0  22782  chfacfpmmulgsum  22784  connclo  23335  dissnlocfin  23449  ptpjpre2  23500  txindis  23554  snfil  23784  alexsublem  23964  tsmsfbas  24048  stdbdxmet  24436  dscmet  24493  xrsxmet  24731  iccpnfcnv  24875  cphsubrglem  25110  minveclem3b  25361  minveclem4a  25363  ovolicc1  25450  dvexp2  25891  dvmptdiv  25911  lhop2  25953  deg1sublt  26048  ig1pval3  26116  dvply1  26224  plydiveu  26239  quotcan  26250  aaliou3lem9  26291  taylthlem2  26315  taylthlem2OLD  26316  pserdvlem2  26371  abelthlem9  26383  logccne0  26520  logtayllem  26601  logtayl  26602  cxpef  26607  rtprmirr  26703  angrtmuld  26751  isosctrlem3  26763  chordthmlem  26775  leibpilem2  26884  leibpi  26885  rlimcnp2  26909  efrlim  26912  efrlimOLD  26913  vma1  27109  muinv  27136  lgsval2lem  27251  lgsval4  27261  lgsdir  27276  lgseisenlem4  27322  lgsquadlem1  27324  lgsquad2  27330  m1lgs  27332  2sqlem8a  27369  2sqlem8  27370  2sqcoprm  27379  2sqmod  27380  padicabv  27574  ostth1  27577  ostth3  27582  nolesgn2ores  27617  nogesgn1ores  27619  nosep1o  27626  nosep2o  27627  nosepdmlem  27628  nosepssdm  27631  noresle  27642  nosupbnd1lem3  27655  nosupbnd1lem4  27656  nosupbnd1lem5  27657  nosupbnd1lem6  27658  nosupbnd2lem1  27660  noinfbnd1lem3  27670  noinfbnd1lem4  27671  noinfbnd1lem5  27672  noinfbnd1lem6  27673  noinfbnd2lem1  27675  0elold  27859  elnnzs  28329  expsnnval  28353  expsne0  28363  tgbtwnne  28470  tgbtwndiff  28486  tgcolg  28534  tgbtwnconn1lem3  28554  legso  28579  tglineeltr  28611  tglineintmo  28622  tglineneq  28624  colline  28629  mirne  28647  miriso  28650  mirhl  28659  mirbtwnhl  28660  symquadlem  28669  krippenlem  28670  midexlem  28672  ragncol  28689  footexALT  28698  footexlem2  28700  colperp  28709  colperpexlem3  28712  mideulem2  28714  opphllem  28715  midex  28717  opptgdim2  28725  oppperpex  28733  hlpasch  28736  colopp  28749  lmieu  28764  trgcopy  28784  cgracol  28808  cgrg3col4  28833  axlowdimlem15  28936  axcontlem2  28945  axcontlem7  28950  1egrvtxdg0  29492  2pthnloop  29711  cyclnspth  29781  eupth2lem1  30197  eupth2lem2  30198  eupth2lem3lem6  30212  nrt2irr  30452  strlem6  32235  hstrlem6  32243  atssma  32357  chirredlem1  32369  snsssng  32493  ifnetrue  32526  ifnefals  32527  fmptunsnop  32673  xaddeq0  32726  rexmul2  32727  xlt2addrd  32732  xnn0nn0d  32745  fzone1  32773  hashpss  32784  elq2  32786  divnumden2  32790  sgnmul  32810  sgn0bi  32815  2exple2exp  32820  chnub  32984  pmtridf1o  33066  pmtridfv1  33067  pmtridfv2  33068  elrgspnlem2  33210  elrgspnlem3  33211  fracfld  33274  pidlnz  33340  lindssn  33342  drngidl  33397  drngidlhash  33398  0ringprmidl  33413  qsidomlem1  33416  ssdifidlprm  33422  mxidlmaxv  33432  mxidlprm  33434  mxidlirredi  33435  mxidlirred  33436  krull  33443  rsprprmprmidlb  33487  rprmasso2  33490  pidufd  33507  1arithufdlem3  33510  dfufd2  33514  zringidom  33515  0ringmon1p  33519  ig1pnunit  33559  lindsunlem  33613  fldextrspundgdvdslem  33668  fldext2rspun  33670  ply1annnr  33686  fldext2chn  33711  constrextdg2lem  33731  constrext2chnlem  33733  constrcon  33757  2sqr3minply  33763  cos9thpiminply  33771  1smat1  33787  submatminr1  33793  madjusmdetlem2  33811  zarcls1  33852  zarclsint  33855  zarclssn  33856  xrge0iifcnv  33916  xrge0iifcv  33917  xrge0iif1  33921  qqhval2lem  33964  qqhf  33969  qqhre  34003  esumrnmpt2  34051  esumcvgre  34074  inelpisys  34137  carsgclctunlem2  34303  ballotlemirc  34516  signswlid  34543  repr0  34595  reprlt  34603  reprgt  34605  reprinfz1  34606  tgoldbachgtda  34645  tgoldbachgt  34647  bnj1523  35054  acycgr2v  35130  fmlaomn0  35370  fmlasucdisj  35379  fz0n  35711  dfrdg2  35776  dfrdg4  35932  broutsideof2  36103  outsidele  36113  rankeq1o  36152  ivthALT  36316  limsucncmpi  36426  topdifinffinlem  37328  icorempo  37332  finxpreclem2  37371  finxp1o  37373  finxpreclem6  37377  poimirlem9  37616  poimirlem11  37618  poimirlem12  37619  poimirlem25  37632  fdc  37732  heibor1lem  37796  heiborlem4  37801  heiborlem6  37803  disjressuc2  38367  2atm  39514  lhpocnle  40003  lhp2at0nle  40022  trlval3  40174  cdleme18c  40280  cdlemg17b  40649  cdlemg17i  40656  dia2dimlem2  41052  dia2dimlem3  41053  dihord6apre  41243  dihatlat  41321  dochshpsat  41441  lcfrlem9  41537  mapdhval2  41713  hdmap1val2  41787  hdmap14lem4a  41858  hdmap14lem6  41860  dvrelogpow2b  42049  aks4d1p1p4  42052  aks4d1p6  42062  fldhmf1  42071  primrootspoweq0  42087  aks6d1c2p2  42100  hashscontpow  42103  aks6d1c5  42120  sticksstones1  42127  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  aks6d1c6lem4  42154  aks6d1c7lem1  42161  aks6d1c7  42165  aks5lem8  42182  negn0nposznnd  42263  mhpind  42575  prjspner1  42607  dffltz  42615  3cubeslem2  42666  jm2.26lem3  42983  kelac1  43045  cantnfresb  43306  tfsconcat0b  43328  nlimsuc  43423  clsk1indlem0  44023  scotteld  44228  sineq0ALT  44919  refsum2cnlem1  45024  disjxp1  45056  nelrnmpt  45071  disjf1  45170  disjrnmpt2  45175  disjinfi  45179  oddfl  45269  xrlttri5d  45275  supxrge  45327  nepnfltpnf  45331  nemnftgtmnft  45333  xrlexaddrp  45341  xrred  45354  supminfxr2  45458  icoiccdif  45515  qinioo  45526  ioonct  45528  fmul01lt1lem1  45575  climrec  45594  limcperiod  45619  reclimc  45644  limsupub  45695  liminflbuz2  45806  cncfiooicclem1  45884  cncfioobdlem  45887  fperdvper  45910  dvdivbd  45914  ditgeqiooicc  45951  itgsincmulx  45965  itgioocnicc  45968  iblcncfioo  45969  stoweidlem35  46026  stoweidlem39  46030  stirlinglem5  46069  stirlinglem8  46072  dirkerper  46087  dirkercncflem2  46095  dirkercncflem4  46097  fourierdlem31  46129  fourierdlem34  46132  fourierdlem41  46139  fourierdlem42  46140  fourierdlem44  46142  fourierdlem48  46145  fourierdlem49  46146  fourierdlem53  46150  fourierdlem56  46153  fourierdlem58  46155  fourierdlem60  46157  fourierdlem61  46158  fourierdlem62  46159  fourierdlem65  46162  fourierdlem66  46163  fourierdlem73  46170  fourierdlem76  46173  fourierdlem79  46176  fourierdlem81  46178  fourierdlem82  46179  fourierdlem93  46190  fourierdlem103  46200  fourierdlem104  46201  sqwvfoura  46219  fourierswlem  46221  elaa2lem  46224  elaa2  46225  etransclem4  46229  etransclem24  46249  etransclem31  46256  etransclem32  46257  etransclem35  46260  sge0repnf  46377  sge0fodjrnlem  46407  sge0iunmpt  46409  sge0rpcpnf  46412  nnfoctbdjlem  46446  meadjun  46453  voliunsge0lem  46463  hoicvr  46539  ovnn0val  46542  ovnsubaddlem1  46561  hoidmvn0val  46575  hsphoidmvle  46577  hoidmv1lelem1  46582  hoidmv1lelem2  46583  hoidmv1lelem3  46584  ovnhoilem1  46592  ovnsubadd2lem  46636  ovnovollem3  46649  cjnpoly  46883  lighneallem3  47601  divgcdoddALTV  47676  isubgr0uhgr  47866  usgrexmpl2trifr  48021  gpg5nbgrvtx03star  48064  gpg5nbgr3star  48065  dignn0flhalflem1  48597  itcoval2  48646  itcoval3  48647  itcovalsuc  48649  ackvalsuc1mpt  48660  line2xlem  48735