Theorem neneqd 3023

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3018

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 209  df-ne 3019

This theorem is referenced by:  neneq  3024  necon2bi  3048  necon2i  3052  necon4i  3053  pm2.21ddne  3103  mteqand  3124  nelrdva  3698  eldifsnneq  4725  disjprg  5064  0inp0  5261  onnseq  7983  sniffsupp  8875  dfac2b  9558  ackbij1lem15  9658  ttukeylem7  9939  fpwwe2lem13  10066  canthnumlem  10072  canthp1lem2  10077  recgt0  11488  nnneneg  11675  elnnz  11994  xrnemnf  12515  xrnepnf  12516  fzprval  12971  fzodisjsn  13078  expnnval  13435  znsqcld  13529  hashelne0d  13732  elprchashprn2  13760  relexpsucnnr  14386  relexp1g  14387  relexpuzrel  14413  sgnp  14451  fprodn0f  15347  ruclem12  15596  dvdsle  15662  nndvdslegcd  15856  gcdnncl  15858  divgcdnn  15865  sqgcd  15911  eucalgf  15929  eucalginv  15930  lcmgcdlem  15952  lcmftp  15982  lcmfunsnlem2lem1  15984  lcmfunsnlem2lem2  15985  qredeu  16004  rpdvds  16006  cncongr2  16014  divnumden  16090  divdenle  16091  phisum  16129  oddprm  16149  pythagtriplem4  16158  pythagtriplem8  16162  pythagtriplem9  16163  4sqlem10  16285  ram0  16360  isipodrs  17773  gsumval2  17898  smndex1n0mnd  18079  smndex2dnrinv  18082  mulgnn  18234  sylow1lem1  18725  gsumval3eu  19026  ablsimpgfindlem1  19231  ablsimpgfindlem2  19232  ablsimpgfind  19234  fincygsubgodd  19236  abvtrivd  19613  00lss  19715  lvecvscan2  19886  fidomndrng  20082  mvrcl  20231  mplmon  20246  mplmonmul  20247  coe1tmfv2  20445  cply1coe0  20469  cply1coe0bi  20470  prmirredlem  20642  uvcff  20937  1marepvsma1  21194  mdetrsca2  21215  mdetrlin2  21218  mdetunilem2  21224  mdetunilem5  21227  mdetunilem6  21228  mdetunilem9  21231  maducoeval2  21251  gsummatr01lem3  21268  gsummatr01lem4  21269  gsummatr01  21270  m2cpm  21351  m2cpminvid2lem  21364  fvmptnn04ifa  21460  fvmptnn04ifb  21461  fvmptnn04ifc  21462  chfacffsupp  21466  chfacfscmul0  21468  chfacfscmulgsum  21470  chfacfpmmul0  21472  chfacfpmmulgsum  21474  connclo  22025  dissnlocfin  22139  ptpjpre2  22190  txindis  22244  snfil  22474  alexsublem  22654  tsmsfbas  22738  stdbdxmet  23127  dscmet  23184  xrsxmet  23419  iccpnfcnv  23550  cphsubrglem  23783  minveclem3b  24033  minveclem4a  24035  ovolicc1  24119  dvexp2  24553  dvmptdiv  24573  lhop2  24614  deg1sublt  24706  ig1pval3  24770  dvply1  24875  plydiveu  24889  quotcan  24900  aaliou3lem9  24941  taylthlem2  24964  pserdvlem2  25018  abelthlem9  25030  logccne0  25164  logtayllem  25244  logtayl  25245  cxpef  25250  angrtmuld  25388  isosctrlem3  25400  chordthmlem  25412  leibpilem2  25521  leibpi  25522  rlimcnp2  25546  efrlim  25549  vma1  25745  muinv  25772  lgsval2lem  25885  lgsval4  25895  lgsdir  25910  lgseisenlem4  25956  lgsquadlem1  25958  lgsquad2  25964  m1lgs  25966  2sqlem8a  26003  2sqlem8  26004  2sqcoprm  26013  2sqmod  26014  padicabv  26208  ostth1  26211  ostth3  26216  tgbtwnne  26278  tgbtwndiff  26294  tgcolg  26342  tgbtwnconn1lem3  26362  legso  26387  tglineeltr  26419  tglineintmo  26430  tglineneq  26432  colline  26437  mirne  26455  miriso  26458  mirhl  26467  mirbtwnhl  26468  symquadlem  26477  krippenlem  26478  midexlem  26480  ragncol  26497  footexALT  26506  footexlem2  26508  colperp  26517  colperpexlem3  26520  mideulem2  26522  opphllem  26523  midex  26525  opptgdim2  26533  oppperpex  26541  hlpasch  26544  colopp  26557  lmieu  26572  trgcopy  26592  cgracol  26616  cgrg3col4  26641  axlowdimlem15  26744  axcontlem2  26753  axcontlem7  26758  1egrvtxdg0  27295  2pthnloop  27514  cyclnspth  27583  eupth2lem1  27999  eupth2lem2  28000  eupth2lem3lem6  28014  strlem6  30035  hstrlem6  30043  atssma  30157  chirredlem1  30169  xaddeq0  30479  xlt2addrd  30484  fzone1  30525  divnumden2  30536  submomnd  30713  pmtridf1o  30738  pmtridfv1  30739  pmtridfv2  30740  ornglmullt  30882  orngrmullt  30883  ofldchr  30889  suborng  30890  lindssn  30941  qsidomlem1  30967  mxidlprm  30979  krull  30982  lindsunlem  31022  1smat1  31071  submatminr1  31077  madjusmdetlem2  31095  xrge0iifcnv  31178  xrge0iifcv  31179  xrge0iif1  31183  qqhval2lem  31224  qqhf  31229  qqhre  31263  esumrnmpt2  31329  esumcvgre  31352  inelpisys  31415  carsgclctunlem2  31579  ballotlemirc  31791  sgnmul  31802  sgn0bi  31807  signswlid  31831  repr0  31884  reprlt  31892  reprgt  31894  reprinfz1  31895  tgoldbachgtda  31934  tgoldbachgt  31936  bnj1523  32345  acycgr2v  32399  fmlaomn0  32639  fmlasucdisj  32648  fz0n  32964  dfrdg2  33042  nolesgn2ores  33181  nosep1o  33188  nosepdmlem  33189  nosepssdm  33192  noresle  33202  nosupbnd1lem3  33212  nosupbnd1lem4  33213  nosupbnd1lem5  33214  nosupbnd1lem6  33215  nosupbnd2lem1  33217  dfrdg4  33414  broutsideof2  33585  outsidele  33595  rankeq1o  33634  ivthALT  33685  limsucncmpi  33795  topdifinffinlem  34630  icorempo  34634  finxpreclem2  34673  finxp1o  34675  finxpreclem6  34679  poimirlem9  34903  poimirlem11  34905  poimirlem12  34906  poimirlem25  34919  fdc  35022  heibor1lem  35089  heiborlem4  35094  heiborlem6  35096  2atm  36665  lhpocnle  37154  lhp2at0nle  37173  trlval3  37325  cdleme18c  37431  cdlemg17b  37800  cdlemg17i  37807  dia2dimlem2  38203  dia2dimlem3  38204  dihord6apre  38394  dihatlat  38472  dochshpsat  38592  lcfrlem9  38688  mapdhval2  38864  hdmap1val2  38938  hdmap14lem4a  39009  hdmap14lem6  39011  negn0nposznnd  39175  nn0rppwr  39189  rtprmirr  39201  dffltz  39278  3cubeslem2  39289  jm2.26lem3  39605  kelac1  39670  clsk1indlem0  40398  scotteld  40589  sineq0ALT  41278  refsum2cnlem1  41301  disjxp1  41338  nelrnmpt  41355  disjf1  41450  disjrnmpt2  41456  disjinfi  41461  rnmptn0  41491  oddfl  41550  xrlttri5d  41556  supxrge  41613  nepnfltpnf  41617  nemnftgtmnft  41619  xrlexaddrp  41627  xrred  41640  supminfxr2  41752  icoiccdif  41807  qinioo  41818  ioonct  41820  fmul01lt1lem1  41872  climrec  41891  limcperiod  41916  reclimc  41941  limsupub  41992  liminflbuz2  42103  cncfiooicclem1  42183  cncfioobdlem  42186  fperdvper  42210  dvdivbd  42215  ditgeqiooicc  42252  itgsincmulx  42266  itgioocnicc  42269  iblcncfioo  42270  stoweidlem35  42327  stoweidlem39  42331  stirlinglem5  42370  stirlinglem8  42373  dirkerper  42388  dirkercncflem2  42396  dirkercncflem4  42398  fourierdlem31  42430  fourierdlem34  42433  fourierdlem41  42440  fourierdlem42  42441  fourierdlem44  42443  fourierdlem48  42446  fourierdlem49  42447  fourierdlem53  42451  fourierdlem56  42454  fourierdlem58  42456  fourierdlem60  42458  fourierdlem61  42459  fourierdlem62  42460  fourierdlem65  42463  fourierdlem66  42464  fourierdlem73  42471  fourierdlem76  42474  fourierdlem79  42477  fourierdlem81  42479  fourierdlem82  42480  fourierdlem93  42491  fourierdlem103  42501  fourierdlem104  42502  sqwvfoura  42520  fourierswlem  42522  elaa2lem  42525  elaa2  42526  etransclem4  42530  etransclem24  42550  etransclem31  42557  etransclem32  42558  etransclem35  42561  sge0repnf  42675  sge0fodjrnlem  42705  sge0iunmpt  42707  sge0rpcpnf  42710  nnfoctbdjlem  42744  meadjun  42751  voliunsge0lem  42761  hoicvr  42837  ovnn0val  42840  ovnsubaddlem1  42859  hoidmvn0val  42873  hsphoidmvle  42875  hoidmv1lelem1  42880  hoidmv1lelem2  42881  hoidmv1lelem3  42882  ovnhoilem1  42890  ovnsubadd2lem  42934  ovnovollem3  42947  lighneallem3  43779  divgcdoddALTV  43854  dignn0flhalflem1  44682  line2xlem  44747