Theorem neneqd 2951

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

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

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 2947

This theorem is referenced by:  neneq  2952  necon2bi  2977  necon2i  2981  necon4i  2982  pm2.21ddne  3032  mteqand  3039  nelrdva  3727  eldifsnneq  4816  disjprg  5162  0inp0  5377  rnmptn0  6275  frxp2  8185  frxp3  8192  onnseq  8400  sniffsupp  9469  dfac2b  10200  ackbij1lem15  10302  ttukeylem7  10584  fpwwe2lem12  10711  canthnumlem  10717  canthp1lem2  10722  recgt0  12140  nnneneg  12328  elnnz  12649  xrnemnf  13180  xrnepnf  13181  fzprval  13645  fzodisjsn  13754  expnnval  14115  znsqcld  14212  hashelne0d  14417  elprchashprn2  14445  relexpsucnnr  15074  relexp1g  15075  relexpuzrel  15101  sgnp  15139  fprodn0f  16039  ruclem12  16289  dvdsle  16358  nndvdslegcd  16551  gcdnncl  16553  divgcdnn  16561  nn0rppwr  16608  sqgcd  16609  eucalgf  16630  eucalginv  16631  lcmgcdlem  16653  lcmftp  16683  lcmfunsnlem2lem1  16685  lcmfunsnlem2lem2  16686  qredeu  16705  rpdvds  16707  cncongr2  16715  divnumden  16795  divdenle  16796  phisum  16837  oddprm  16857  pythagtriplem4  16866  pythagtriplem8  16870  pythagtriplem9  16871  4sqlem10  16994  ram0  17069  cat1lem  18163  isipodrs  18607  gsumval2  18724  smndex1n0mnd  18947  smndex2dnrinv  18950  mulgnn  19115  sylow1lem1  19640  gsumval3eu  19946  ablsimpgfindlem1  20151  ablsimpgfindlem2  20152  ablsimpgfind  20154  fincygsubgodd  20156  rrgnz  20726  fidomndrng  20796  abvtrivd  20855  00lss  20962  lvecvscan2  21137  prmirredlem  21506  uvcff  21834  mvrcl  22035  mplmon  22076  mplmonmul  22077  psdmul  22193  coe1tmfv2  22299  cply1coe0  22326  cply1coe0bi  22327  1marepvsma1  22610  mdetrsca2  22631  mdetrlin2  22634  mdetunilem2  22640  mdetunilem5  22643  mdetunilem6  22644  mdetunilem9  22647  maducoeval2  22667  gsummatr01lem3  22684  gsummatr01lem4  22685  gsummatr01  22686  m2cpm  22768  m2cpminvid2lem  22781  fvmptnn04ifa  22877  fvmptnn04ifb  22878  fvmptnn04ifc  22879  chfacffsupp  22883  chfacfscmul0  22885  chfacfscmulgsum  22887  chfacfpmmul0  22889  chfacfpmmulgsum  22891  connclo  23444  dissnlocfin  23558  ptpjpre2  23609  txindis  23663  snfil  23893  alexsublem  24073  tsmsfbas  24157  stdbdxmet  24549  dscmet  24606  xrsxmet  24850  iccpnfcnv  24994  cphsubrglem  25230  minveclem3b  25481  minveclem4a  25483  ovolicc1  25570  dvexp2  26012  dvmptdiv  26032  lhop2  26074  deg1sublt  26169  ig1pval3  26237  dvply1  26343  plydiveu  26358  quotcan  26369  aaliou3lem9  26410  taylthlem2  26434  taylthlem2OLD  26435  pserdvlem2  26490  abelthlem9  26502  logccne0  26638  logtayllem  26719  logtayl  26720  cxpef  26725  rtprmirr  26821  angrtmuld  26869  isosctrlem3  26881  chordthmlem  26893  leibpilem2  27002  leibpi  27003  rlimcnp2  27027  efrlim  27030  efrlimOLD  27031  vma1  27227  muinv  27254  lgsval2lem  27369  lgsval4  27379  lgsdir  27394  lgseisenlem4  27440  lgsquadlem1  27442  lgsquad2  27448  m1lgs  27450  2sqlem8a  27487  2sqlem8  27488  2sqcoprm  27497  2sqmod  27498  padicabv  27692  ostth1  27695  ostth3  27700  nolesgn2ores  27735  nogesgn1ores  27737  nosep1o  27744  nosep2o  27745  nosepdmlem  27746  nosepssdm  27749  noresle  27760  nosupbnd1lem3  27773  nosupbnd1lem4  27774  nosupbnd1lem5  27775  nosupbnd1lem6  27776  nosupbnd2lem1  27778  noinfbnd1lem3  27788  noinfbnd1lem4  27789  noinfbnd1lem5  27790  noinfbnd1lem6  27791  noinfbnd2lem1  27793  0elold  27965  elnnzs  28405  expsnnval  28427  expsne0  28432  tgbtwnne  28516  tgbtwndiff  28532  tgcolg  28580  tgbtwnconn1lem3  28600  legso  28625  tglineeltr  28657  tglineintmo  28668  tglineneq  28670  colline  28675  mirne  28693  miriso  28696  mirhl  28705  mirbtwnhl  28706  symquadlem  28715  krippenlem  28716  midexlem  28718  ragncol  28735  footexALT  28744  footexlem2  28746  colperp  28755  colperpexlem3  28758  mideulem2  28760  opphllem  28761  midex  28763  opptgdim2  28771  oppperpex  28779  hlpasch  28782  colopp  28795  lmieu  28810  trgcopy  28830  cgracol  28854  cgrg3col4  28879  axlowdimlem15  28989  axcontlem2  28998  axcontlem7  29003  1egrvtxdg0  29547  2pthnloop  29767  cyclnspth  29836  eupth2lem1  30250  eupth2lem2  30251  eupth2lem3lem6  30265  nrt2irr  30505  strlem6  32288  hstrlem6  32296  atssma  32410  chirredlem1  32422  snsssng  32543  ifnetrue  32570  ifnefals  32571  xaddeq0  32760  xlt2addrd  32765  fzone1  32805  divnumden2  32819  chnub  32984  submomnd  33060  pmtridf1o  33087  pmtridfv1  33088  pmtridfv2  33089  fracfld  33275  ornglmullt  33302  orngrmullt  33303  ofldchr  33309  suborng  33310  pidlnz  33369  lindssn  33371  drngidl  33426  drngidlhash  33427  0ringprmidl  33442  qsidomlem1  33445  ssdifidlprm  33451  mxidlmaxv  33461  mxidlprm  33463  mxidlirredi  33464  mxidlirred  33465  krull  33472  rsprprmprmidlb  33516  rprmasso2  33519  pidufd  33536  1arithufdlem3  33539  dfufd2  33543  zringidom  33544  0ringmon1p  33548  ig1pnunit  33586  lindsunlem  33637  ply1annnr  33696  fldext2chn  33719  2sqr3minply  33738  1smat1  33750  submatminr1  33756  madjusmdetlem2  33774  zarcls1  33815  zarclsint  33818  zarclssn  33819  xrge0iifcnv  33879  xrge0iifcv  33880  xrge0iif1  33884  qqhval2lem  33927  qqhf  33932  qqhre  33966  esumrnmpt2  34032  esumcvgre  34055  inelpisys  34118  carsgclctunlem2  34284  ballotlemirc  34496  sgnmul  34507  sgn0bi  34512  signswlid  34536  repr0  34588  reprlt  34596  reprgt  34598  reprinfz1  34599  tgoldbachgtda  34638  tgoldbachgt  34640  bnj1523  35047  acycgr2v  35118  fmlaomn0  35358  fmlasucdisj  35367  fz0n  35693  dfrdg2  35759  dfrdg4  35915  broutsideof2  36086  outsidele  36096  rankeq1o  36135  ivthALT  36301  limsucncmpi  36411  topdifinffinlem  37313  icorempo  37317  finxpreclem2  37356  finxp1o  37358  finxpreclem6  37362  poimirlem9  37589  poimirlem11  37591  poimirlem12  37592  poimirlem25  37605  fdc  37705  heibor1lem  37769  heiborlem4  37774  heiborlem6  37776  disjressuc2  38344  2atm  39484  lhpocnle  39973  lhp2at0nle  39992  trlval3  40144  cdleme18c  40250  cdlemg17b  40619  cdlemg17i  40626  dia2dimlem2  41022  dia2dimlem3  41023  dihord6apre  41213  dihatlat  41291  dochshpsat  41411  lcfrlem9  41507  mapdhval2  41683  hdmap1val2  41757  hdmap14lem4a  41828  hdmap14lem6  41830  dvrelogpow2b  42025  aks4d1p1p4  42028  aks4d1p6  42038  fldhmf1  42047  primrootspoweq0  42063  aks6d1c2p2  42076  hashscontpow  42079  aks6d1c5  42096  sticksstones1  42103  sticksstones10  42112  sticksstones12a  42114  sticksstones12  42115  sticksstones22  42125  aks6d1c6lem4  42130  aks6d1c7lem1  42137  aks6d1c7  42141  aks5lem8  42158  metakunt6  42167  metakunt7  42168  metakunt11  42172  metakunt12  42173  metakunt27  42188  metakunt28  42189  metakunt29  42190  metakunt30  42191  negn0nposznnd  42271  mhpind  42549  prjspner1  42581  dffltz  42589  3cubeslem2  42641  jm2.26lem3  42958  kelac1  43020  cantnfresb  43286  tfsconcat0b  43308  nlimsuc  43403  clsk1indlem0  44003  finnzfsuppd  44171  scotteld  44215  sineq0ALT  44908  refsum2cnlem1  44937  disjxp1  44971  nelrnmpt  44986  disjf1  45090  disjrnmpt2  45095  disjinfi  45099  oddfl  45192  xrlttri5d  45198  supxrge  45253  nepnfltpnf  45257  nemnftgtmnft  45259  xrlexaddrp  45267  xrred  45280  supminfxr2  45384  icoiccdif  45442  qinioo  45453  ioonct  45455  fmul01lt1lem1  45505  climrec  45524  limcperiod  45549  reclimc  45574  limsupub  45625  liminflbuz2  45736  cncfiooicclem1  45814  cncfioobdlem  45817  fperdvper  45840  dvdivbd  45844  ditgeqiooicc  45881  itgsincmulx  45895  itgioocnicc  45898  iblcncfioo  45899  stoweidlem35  45956  stoweidlem39  45960  stirlinglem5  45999  stirlinglem8  46002  dirkerper  46017  dirkercncflem2  46025  dirkercncflem4  46027  fourierdlem31  46059  fourierdlem34  46062  fourierdlem41  46069  fourierdlem42  46070  fourierdlem44  46072  fourierdlem48  46075  fourierdlem49  46076  fourierdlem53  46080  fourierdlem56  46083  fourierdlem58  46085  fourierdlem60  46087  fourierdlem61  46088  fourierdlem62  46089  fourierdlem65  46092  fourierdlem66  46093  fourierdlem73  46100  fourierdlem76  46103  fourierdlem79  46106  fourierdlem81  46108  fourierdlem82  46109  fourierdlem93  46120  fourierdlem103  46130  fourierdlem104  46131  sqwvfoura  46149  fourierswlem  46151  elaa2lem  46154  elaa2  46155  etransclem4  46159  etransclem24  46179  etransclem31  46186  etransclem32  46187  etransclem35  46190  sge0repnf  46307  sge0fodjrnlem  46337  sge0iunmpt  46339  sge0rpcpnf  46342  nnfoctbdjlem  46376  meadjun  46383  voliunsge0lem  46393  hoicvr  46469  ovnn0val  46472  ovnsubaddlem1  46491  hoidmvn0val  46505  hsphoidmvle  46507  hoidmv1lelem1  46512  hoidmv1lelem2  46513  hoidmv1lelem3  46514  ovnhoilem1  46522  ovnsubadd2lem  46566  ovnovollem3  46579  lighneallem3  47481  divgcdoddALTV  47556  isubgr0uhgr  47743  usgrexmpl2trifr  47852  dignn0flhalflem1  48349  itcoval2  48398  itcoval3  48399  itcovalsuc  48401  ackvalsuc1mpt  48412  line2xlem  48487