Theorem neneqd 2931

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1540   ≠ wne 2926

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 2927

This theorem is referenced by:  neneq  2932  necon2bi  2956  necon2i  2960  necon4i  2961  pm2.21ddne  3010  mteqand  3017  nelrdva  3679  eldifsnneq  4758  disjprg  5106  0inp0  5317  rnmptn0  6220  resf1extb  7913  frxp2  8126  frxp3  8133  onnseq  8316  finnzfsuppd  9331  sniffsupp  9358  dfac2b  10091  ackbij1lem15  10193  ttukeylem7  10475  fpwwe2lem12  10602  canthnumlem  10608  canthp1lem2  10613  recgt0  12035  nnneneg  12228  elnnz  12546  xrnemnf  13084  xrnepnf  13085  fzprval  13553  fzodisjsn  13665  expnnval  14036  znsqcld  14134  hashelne0d  14340  elprchashprn2  14368  relexpsucnnr  14998  relexp1g  14999  relexpuzrel  15025  sgnp  15063  fprodn0f  15964  ruclem12  16216  dvdsle  16287  nndvdslegcd  16482  gcdnncl  16484  divgcdnn  16492  nn0rppwr  16538  sqgcd  16539  eucalgf  16560  eucalginv  16561  lcmgcdlem  16583  lcmftp  16613  lcmfunsnlem2lem1  16615  lcmfunsnlem2lem2  16616  qredeu  16635  rpdvds  16637  cncongr2  16645  divnumden  16725  divdenle  16726  phisum  16768  oddprm  16788  pythagtriplem4  16797  pythagtriplem8  16801  pythagtriplem9  16802  4sqlem10  16925  ram0  17000  cat1lem  18065  isipodrs  18503  gsumval2  18620  smndex1n0mnd  18846  smndex2dnrinv  18849  mulgnn  19014  sylow1lem1  19535  gsumval3eu  19841  ablsimpgfindlem1  20046  ablsimpgfindlem2  20047  ablsimpgfind  20049  fincygsubgodd  20051  rrgnz  20620  fidomndrng  20689  abvtrivd  20748  00lss  20854  lvecvscan2  21029  prmirredlem  21389  uvcff  21707  mvrcl  21908  mplmon  21949  mplmonmul  21950  psdmul  22060  coe1tmfv2  22168  cply1coe0  22195  cply1coe0bi  22196  1marepvsma1  22477  mdetrsca2  22498  mdetrlin2  22501  mdetunilem2  22507  mdetunilem5  22510  mdetunilem6  22511  mdetunilem9  22514  maducoeval2  22534  gsummatr01lem3  22551  gsummatr01lem4  22552  gsummatr01  22553  m2cpm  22635  m2cpminvid2lem  22648  fvmptnn04ifa  22744  fvmptnn04ifb  22745  fvmptnn04ifc  22746  chfacffsupp  22750  chfacfscmul0  22752  chfacfscmulgsum  22754  chfacfpmmul0  22756  chfacfpmmulgsum  22758  connclo  23309  dissnlocfin  23423  ptpjpre2  23474  txindis  23528  snfil  23758  alexsublem  23938  tsmsfbas  24022  stdbdxmet  24410  dscmet  24467  xrsxmet  24705  iccpnfcnv  24849  cphsubrglem  25084  minveclem3b  25335  minveclem4a  25337  ovolicc1  25424  dvexp2  25865  dvmptdiv  25885  lhop2  25927  deg1sublt  26022  ig1pval3  26090  dvply1  26198  plydiveu  26213  quotcan  26224  aaliou3lem9  26265  taylthlem2  26289  taylthlem2OLD  26290  pserdvlem2  26345  abelthlem9  26357  logccne0  26494  logtayllem  26575  logtayl  26576  cxpef  26581  rtprmirr  26677  angrtmuld  26725  isosctrlem3  26737  chordthmlem  26749  leibpilem2  26858  leibpi  26859  rlimcnp2  26883  efrlim  26886  efrlimOLD  26887  vma1  27083  muinv  27110  lgsval2lem  27225  lgsval4  27235  lgsdir  27250  lgseisenlem4  27296  lgsquadlem1  27298  lgsquad2  27304  m1lgs  27306  2sqlem8a  27343  2sqlem8  27344  2sqcoprm  27353  2sqmod  27354  padicabv  27548  ostth1  27551  ostth3  27556  nolesgn2ores  27591  nogesgn1ores  27593  nosep1o  27600  nosep2o  27601  nosepdmlem  27602  nosepssdm  27605  noresle  27616  nosupbnd1lem3  27629  nosupbnd1lem4  27630  nosupbnd1lem5  27631  nosupbnd1lem6  27632  nosupbnd2lem1  27634  noinfbnd1lem3  27644  noinfbnd1lem4  27645  noinfbnd1lem5  27646  noinfbnd1lem6  27647  noinfbnd2lem1  27649  0elold  27828  elnnzs  28296  expsnnval  28319  expsne0  28328  tgbtwnne  28424  tgbtwndiff  28440  tgcolg  28488  tgbtwnconn1lem3  28508  legso  28533  tglineeltr  28565  tglineintmo  28576  tglineneq  28578  colline  28583  mirne  28601  miriso  28604  mirhl  28613  mirbtwnhl  28614  symquadlem  28623  krippenlem  28624  midexlem  28626  ragncol  28643  footexALT  28652  footexlem2  28654  colperp  28663  colperpexlem3  28666  mideulem2  28668  opphllem  28669  midex  28671  opptgdim2  28679  oppperpex  28687  hlpasch  28690  colopp  28703  lmieu  28718  trgcopy  28738  cgracol  28762  cgrg3col4  28787  axlowdimlem15  28890  axcontlem2  28899  axcontlem7  28904  1egrvtxdg0  29446  2pthnloop  29668  cyclnspth  29738  eupth2lem1  30154  eupth2lem2  30155  eupth2lem3lem6  30169  nrt2irr  30409  strlem6  32192  hstrlem6  32200  atssma  32314  chirredlem1  32326  snsssng  32450  ifnetrue  32483  ifnefals  32484  fmptunsnop  32630  xaddeq0  32683  rexmul2  32684  xlt2addrd  32689  xnn0nn0d  32702  fzone1  32730  hashpss  32741  elq2  32743  divnumden2  32747  sgnmul  32767  sgn0bi  32772  2exple2exp  32777  chnub  32945  submomnd  33031  pmtridf1o  33058  pmtridfv1  33059  pmtridfv2  33060  elrgspnlem2  33201  elrgspnlem3  33202  fracfld  33265  ornglmullt  33292  orngrmullt  33293  ofldchr  33299  suborng  33300  pidlnz  33354  lindssn  33356  drngidl  33411  drngidlhash  33412  0ringprmidl  33427  qsidomlem1  33430  ssdifidlprm  33436  mxidlmaxv  33446  mxidlprm  33448  mxidlirredi  33449  mxidlirred  33450  krull  33457  rsprprmprmidlb  33501  rprmasso2  33504  pidufd  33521  1arithufdlem3  33524  dfufd2  33528  zringidom  33529  0ringmon1p  33533  ig1pnunit  33573  lindsunlem  33627  fldextrspundgdvdslem  33682  fldext2rspun  33684  ply1annnr  33700  fldext2chn  33725  constrextdg2lem  33745  constrext2chnlem  33747  constrcon  33771  2sqr3minply  33777  cos9thpiminply  33785  1smat1  33801  submatminr1  33807  madjusmdetlem2  33825  zarcls1  33866  zarclsint  33869  zarclssn  33870  xrge0iifcnv  33930  xrge0iifcv  33931  xrge0iif1  33935  qqhval2lem  33978  qqhf  33983  qqhre  34017  esumrnmpt2  34065  esumcvgre  34088  inelpisys  34151  carsgclctunlem2  34317  ballotlemirc  34530  signswlid  34557  repr0  34609  reprlt  34617  reprgt  34619  reprinfz1  34620  tgoldbachgtda  34659  tgoldbachgt  34661  bnj1523  35068  acycgr2v  35144  fmlaomn0  35384  fmlasucdisj  35393  fz0n  35725  dfrdg2  35790  dfrdg4  35946  broutsideof2  36117  outsidele  36127  rankeq1o  36166  ivthALT  36330  limsucncmpi  36440  topdifinffinlem  37342  icorempo  37346  finxpreclem2  37385  finxp1o  37387  finxpreclem6  37391  poimirlem9  37630  poimirlem11  37632  poimirlem12  37633  poimirlem25  37646  fdc  37746  heibor1lem  37810  heiborlem4  37815  heiborlem6  37817  disjressuc2  38381  2atm  39528  lhpocnle  40017  lhp2at0nle  40036  trlval3  40188  cdleme18c  40294  cdlemg17b  40663  cdlemg17i  40670  dia2dimlem2  41066  dia2dimlem3  41067  dihord6apre  41257  dihatlat  41335  dochshpsat  41455  lcfrlem9  41551  mapdhval2  41727  hdmap1val2  41801  hdmap14lem4a  41872  hdmap14lem6  41874  dvrelogpow2b  42063  aks4d1p1p4  42066  aks4d1p6  42076  fldhmf1  42085  primrootspoweq0  42101  aks6d1c2p2  42114  hashscontpow  42117  aks6d1c5  42134  sticksstones1  42141  sticksstones10  42150  sticksstones12a  42152  sticksstones12  42153  sticksstones22  42163  aks6d1c6lem4  42168  aks6d1c7lem1  42175  aks6d1c7  42179  aks5lem8  42196  negn0nposznnd  42277  mhpind  42589  prjspner1  42621  dffltz  42629  3cubeslem2  42680  jm2.26lem3  42997  kelac1  43059  cantnfresb  43320  tfsconcat0b  43342  nlimsuc  43437  clsk1indlem0  44037  scotteld  44242  sineq0ALT  44933  refsum2cnlem1  45038  disjxp1  45070  nelrnmpt  45085  disjf1  45184  disjrnmpt2  45189  disjinfi  45193  oddfl  45283  xrlttri5d  45289  supxrge  45341  nepnfltpnf  45345  nemnftgtmnft  45347  xrlexaddrp  45355  xrred  45368  supminfxr2  45472  icoiccdif  45529  qinioo  45540  ioonct  45542  fmul01lt1lem1  45589  climrec  45608  limcperiod  45633  reclimc  45658  limsupub  45709  liminflbuz2  45820  cncfiooicclem1  45898  cncfioobdlem  45901  fperdvper  45924  dvdivbd  45928  ditgeqiooicc  45965  itgsincmulx  45979  itgioocnicc  45982  iblcncfioo  45983  stoweidlem35  46040  stoweidlem39  46044  stirlinglem5  46083  stirlinglem8  46086  dirkerper  46101  dirkercncflem2  46109  dirkercncflem4  46111  fourierdlem31  46143  fourierdlem34  46146  fourierdlem41  46153  fourierdlem42  46154  fourierdlem44  46156  fourierdlem48  46159  fourierdlem49  46160  fourierdlem53  46164  fourierdlem56  46167  fourierdlem58  46169  fourierdlem60  46171  fourierdlem61  46172  fourierdlem62  46173  fourierdlem65  46176  fourierdlem66  46177  fourierdlem73  46184  fourierdlem76  46187  fourierdlem79  46190  fourierdlem81  46192  fourierdlem82  46193  fourierdlem93  46204  fourierdlem103  46214  fourierdlem104  46215  sqwvfoura  46233  fourierswlem  46235  elaa2lem  46238  elaa2  46239  etransclem4  46243  etransclem24  46263  etransclem31  46270  etransclem32  46271  etransclem35  46274  sge0repnf  46391  sge0fodjrnlem  46421  sge0iunmpt  46423  sge0rpcpnf  46426  nnfoctbdjlem  46460  meadjun  46467  voliunsge0lem  46477  hoicvr  46553  ovnn0val  46556  ovnsubaddlem1  46575  hoidmvn0val  46589  hsphoidmvle  46591  hoidmv1lelem1  46596  hoidmv1lelem2  46597  hoidmv1lelem3  46598  ovnhoilem1  46606  ovnsubadd2lem  46650  ovnovollem3  46663  lighneallem3  47612  divgcdoddALTV  47687  isubgr0uhgr  47877  usgrexmpl2trifr  48032  gpg5nbgrvtx03star  48075  gpg5nbgr3star  48076  dignn0flhalflem1  48608  itcoval2  48657  itcoval3  48658  itcovalsuc  48660  ackvalsuc1mpt  48671  line2xlem  48746