Theorem neneqd 2933

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2928

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 2929

This theorem is referenced by:  neneq  2934  necon2bi  2958  necon2i  2962  necon4i  2963  pm2.21ddne  3012  mteqand  3019  nelrdva  3659  eldifsnneq  4740  disjprg  5085  0inp0  5295  rnmptn0  6191  resf1extb  7864  frxp2  8074  frxp3  8081  onnseq  8264  finnzfsuppd  9257  sniffsupp  9284  dfac2b  10022  ackbij1lem15  10124  ttukeylem7  10406  fpwwe2lem12  10533  canthnumlem  10539  canthp1lem2  10544  recgt0  11967  nnneneg  12160  elnnz  12478  xrnemnf  13016  xrnepnf  13017  fzprval  13485  fzodisjsn  13597  fzone1  13684  expnnval  13971  znsqcld  14069  hashelne0d  14275  elprchashprn2  14303  relexpsucnnr  14932  relexp1g  14933  relexpuzrel  14959  sgnp  14997  fprodn0f  15898  ruclem12  16150  dvdsle  16221  nndvdslegcd  16416  gcdnncl  16418  divgcdnn  16426  nn0rppwr  16472  sqgcd  16473  eucalgf  16494  eucalginv  16495  lcmgcdlem  16517  lcmftp  16547  lcmfunsnlem2lem1  16549  lcmfunsnlem2lem2  16550  qredeu  16569  rpdvds  16571  cncongr2  16579  divnumden  16659  divdenle  16660  phisum  16702  oddprm  16722  pythagtriplem4  16731  pythagtriplem8  16735  pythagtriplem9  16736  4sqlem10  16859  ram0  16934  cat1lem  18003  isipodrs  18443  chnub  18528  chnpof1  18536  gsumval2  18594  smndex1n0mnd  18820  smndex2dnrinv  18823  mulgnn  18988  sylow1lem1  19510  gsumval3eu  19816  ablsimpgfindlem1  20021  ablsimpgfindlem2  20022  ablsimpgfind  20024  fincygsubgodd  20026  submomnd  20044  rrgnz  20619  fidomndrng  20688  abvtrivd  20747  ornglmullt  20784  orngrmullt  20785  suborng  20791  00lss  20874  lvecvscan2  21049  prmirredlem  21409  ofldchr  21513  uvcff  21728  mvrcl  21929  mplmon  21970  mplmonmul  21971  psdmul  22081  coe1tmfv2  22189  cply1coe0  22216  cply1coe0bi  22217  1marepvsma1  22498  mdetrsca2  22519  mdetrlin2  22522  mdetunilem2  22528  mdetunilem5  22531  mdetunilem6  22532  mdetunilem9  22535  maducoeval2  22555  gsummatr01lem3  22572  gsummatr01lem4  22573  gsummatr01  22574  m2cpm  22656  m2cpminvid2lem  22669  fvmptnn04ifa  22765  fvmptnn04ifb  22766  fvmptnn04ifc  22767  chfacffsupp  22771  chfacfscmul0  22773  chfacfscmulgsum  22775  chfacfpmmul0  22777  chfacfpmmulgsum  22779  connclo  23330  dissnlocfin  23444  ptpjpre2  23495  txindis  23549  snfil  23779  alexsublem  23959  tsmsfbas  24043  stdbdxmet  24430  dscmet  24487  xrsxmet  24725  iccpnfcnv  24869  cphsubrglem  25104  minveclem3b  25355  minveclem4a  25357  ovolicc1  25444  dvexp2  25885  dvmptdiv  25905  lhop2  25947  deg1sublt  26042  ig1pval3  26110  dvply1  26218  plydiveu  26233  quotcan  26244  aaliou3lem9  26285  taylthlem2  26309  taylthlem2OLD  26310  pserdvlem2  26365  abelthlem9  26377  logccne0  26514  logtayllem  26595  logtayl  26596  cxpef  26601  rtprmirr  26697  angrtmuld  26745  isosctrlem3  26757  chordthmlem  26769  leibpilem2  26878  leibpi  26879  rlimcnp2  26903  efrlim  26906  efrlimOLD  26907  vma1  27103  muinv  27130  lgsval2lem  27245  lgsval4  27255  lgsdir  27270  lgseisenlem4  27316  lgsquadlem1  27318  lgsquad2  27324  m1lgs  27326  2sqlem8a  27363  2sqlem8  27364  2sqcoprm  27373  2sqmod  27374  padicabv  27568  ostth1  27571  ostth3  27576  nolesgn2ores  27611  nogesgn1ores  27613  nosep1o  27620  nosep2o  27621  nosepdmlem  27622  nosepssdm  27625  noresle  27636  nosupbnd1lem3  27649  nosupbnd1lem4  27650  nosupbnd1lem5  27651  nosupbnd1lem6  27652  nosupbnd2lem1  27654  noinfbnd1lem3  27664  noinfbnd1lem4  27665  noinfbnd1lem5  27666  noinfbnd1lem6  27667  noinfbnd2lem1  27669  0elold  27855  elnnzs  28325  expsnnval  28349  expsne0  28359  tgbtwnne  28468  tgbtwndiff  28484  tgcolg  28532  tgbtwnconn1lem3  28552  legso  28577  tglineeltr  28609  tglineintmo  28620  tglineneq  28622  colline  28627  mirne  28645  miriso  28648  mirhl  28657  mirbtwnhl  28658  symquadlem  28667  krippenlem  28668  midexlem  28670  ragncol  28687  footexALT  28696  footexlem2  28698  colperp  28707  colperpexlem3  28710  mideulem2  28712  opphllem  28713  midex  28715  opptgdim2  28723  oppperpex  28731  hlpasch  28734  colopp  28747  lmieu  28762  trgcopy  28782  cgracol  28806  cgrg3col4  28831  axlowdimlem15  28934  axcontlem2  28943  axcontlem7  28948  1egrvtxdg0  29490  2pthnloop  29709  cyclnspth  29779  eupth2lem1  30198  eupth2lem2  30199  eupth2lem3lem6  30213  nrt2irr  30453  strlem6  32236  hstrlem6  32244  atssma  32358  chirredlem1  32370  snsssng  32494  ifnetrue  32527  ifnefals  32528  fmptunsnop  32681  xaddeq0  32736  rexmul2  32737  xlt2addrd  32742  xnn0nn0d  32755  hashpss  32791  elq2  32794  divnumden2  32798  sgnmul  32818  sgn0bi  32823  2exple2exp  32828  pmtridf1o  33063  pmtridfv1  33064  pmtridfv2  33065  elrgspnlem2  33210  elrgspnlem3  33211  fracfld  33274  pidlnz  33341  lindssn  33343  drngidl  33398  drngidlhash  33399  0ringprmidl  33414  qsidomlem1  33417  ssdifidlprm  33423  mxidlmaxv  33433  mxidlprm  33435  mxidlirredi  33436  mxidlirred  33437  krull  33444  rsprprmprmidlb  33488  rprmasso2  33491  pidufd  33508  1arithufdlem3  33511  dfufd2  33515  zringidom  33516  0ringmon1p  33520  ig1pnunit  33561  esplymhp  33589  lindsunlem  33637  fldextrspundgdvdslem  33693  fldext2rspun  33695  ply1annnr  33716  fldext2chn  33741  constrextdg2lem  33761  constrext2chnlem  33763  constrcon  33787  2sqr3minply  33793  cos9thpiminply  33801  1smat1  33817  submatminr1  33823  madjusmdetlem2  33841  zarcls1  33882  zarclsint  33885  zarclssn  33886  xrge0iifcnv  33946  xrge0iifcv  33947  xrge0iif1  33951  qqhval2lem  33994  qqhf  33999  qqhre  34033  esumrnmpt2  34081  esumcvgre  34104  inelpisys  34167  carsgclctunlem2  34332  ballotlemirc  34545  signswlid  34572  repr0  34624  reprlt  34632  reprgt  34634  reprinfz1  34635  tgoldbachgtda  34674  tgoldbachgt  34676  bnj1523  35083  acycgr2v  35194  fmlaomn0  35434  fmlasucdisj  35443  fz0n  35775  dfrdg2  35837  dfrdg4  35995  broutsideof2  36166  outsidele  36176  rankeq1o  36215  ivthALT  36379  limsucncmpi  36489  topdifinffinlem  37391  icorempo  37395  finxpreclem2  37434  finxp1o  37436  finxpreclem6  37440  poimirlem9  37668  poimirlem11  37670  poimirlem12  37671  poimirlem25  37684  fdc  37784  heibor1lem  37848  heiborlem4  37853  heiborlem6  37855  disjressuc2  38434  2atm  39625  lhpocnle  40114  lhp2at0nle  40133  trlval3  40285  cdleme18c  40391  cdlemg17b  40760  cdlemg17i  40767  dia2dimlem2  41163  dia2dimlem3  41164  dihord6apre  41354  dihatlat  41432  dochshpsat  41552  lcfrlem9  41648  mapdhval2  41824  hdmap1val2  41898  hdmap14lem4a  41969  hdmap14lem6  41971  dvrelogpow2b  42160  aks4d1p1p4  42163  aks4d1p6  42173  fldhmf1  42182  primrootspoweq0  42198  aks6d1c2p2  42211  hashscontpow  42214  aks6d1c5  42231  sticksstones1  42238  sticksstones10  42247  sticksstones12a  42249  sticksstones12  42250  sticksstones22  42260  aks6d1c6lem4  42265  aks6d1c7lem1  42272  aks6d1c7  42276  aks5lem8  42293  negn0nposznnd  42374  mhpind  42686  prjspner1  42718  dffltz  42726  3cubeslem2  42777  jm2.26lem3  43093  kelac1  43155  cantnfresb  43416  tfsconcat0b  43438  nlimsuc  43533  clsk1indlem0  44133  scotteld  44338  sineq0ALT  45028  refsum2cnlem1  45133  disjxp1  45165  nelrnmpt  45180  disjf1  45279  disjrnmpt2  45284  disjinfi  45288  oddfl  45378  xrlttri5d  45384  supxrge  45436  nepnfltpnf  45440  nemnftgtmnft  45442  xrlexaddrp  45450  xrred  45462  supminfxr2  45566  icoiccdif  45623  qinioo  45634  ioonct  45636  fmul01lt1lem1  45683  climrec  45702  limcperiod  45727  reclimc  45750  limsupub  45801  liminflbuz2  45912  cncfiooicclem1  45990  cncfioobdlem  45993  fperdvper  46016  dvdivbd  46020  ditgeqiooicc  46057  itgsincmulx  46071  itgioocnicc  46074  iblcncfioo  46075  stoweidlem35  46132  stoweidlem39  46136  stirlinglem5  46175  stirlinglem8  46178  dirkerper  46193  dirkercncflem2  46201  dirkercncflem4  46203  fourierdlem31  46235  fourierdlem34  46238  fourierdlem41  46245  fourierdlem42  46246  fourierdlem44  46248  fourierdlem48  46251  fourierdlem49  46252  fourierdlem53  46256  fourierdlem56  46259  fourierdlem58  46261  fourierdlem60  46263  fourierdlem61  46264  fourierdlem62  46265  fourierdlem65  46268  fourierdlem66  46269  fourierdlem73  46276  fourierdlem76  46279  fourierdlem79  46282  fourierdlem81  46284  fourierdlem82  46285  fourierdlem93  46296  fourierdlem103  46306  fourierdlem104  46307  sqwvfoura  46325  fourierswlem  46327  elaa2lem  46330  elaa2  46331  etransclem4  46335  etransclem24  46355  etransclem31  46362  etransclem32  46363  etransclem35  46366  sge0repnf  46483  sge0fodjrnlem  46513  sge0iunmpt  46515  sge0rpcpnf  46518  nnfoctbdjlem  46552  meadjun  46559  voliunsge0lem  46569  hoicvr  46645  ovnn0val  46648  ovnsubaddlem1  46667  hoidmvn0val  46681  hsphoidmvle  46683  hoidmv1lelem1  46688  hoidmv1lelem2  46689  hoidmv1lelem3  46690  ovnhoilem1  46698  ovnsubadd2lem  46742  ovnovollem3  46755  cjnpoly  46988  lighneallem3  47706  divgcdoddALTV  47781  isubgr0uhgr  47972  usgrexmpl2trifr  48136  gpg5nbgrvtx03star  48179  gpg5nbgr3star  48180  dignn0flhalflem1  48715  itcoval2  48764  itcoval3  48765  itcovalsuc  48767  ackvalsuc1mpt  48778  line2xlem  48853