Theorem neneqd 2945

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

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

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 2941

This theorem is referenced by:  neneq  2946  necon2bi  2971  necon2i  2975  necon4i  2976  pm2.21ddne  3026  mteqand  3033  nelrdva  3711  eldifsnneq  4791  disjprg  5139  0inp0  5359  rnmptn0  6264  resf1extb  7956  frxp2  8169  frxp3  8176  onnseq  8384  finnzfsuppd  9413  sniffsupp  9440  dfac2b  10171  ackbij1lem15  10273  ttukeylem7  10555  fpwwe2lem12  10682  canthnumlem  10688  canthp1lem2  10693  recgt0  12113  nnneneg  12301  elnnz  12623  xrnemnf  13159  xrnepnf  13160  fzprval  13625  fzodisjsn  13737  expnnval  14105  znsqcld  14202  hashelne0d  14407  elprchashprn2  14435  relexpsucnnr  15064  relexp1g  15065  relexpuzrel  15091  sgnp  15129  fprodn0f  16027  ruclem12  16277  dvdsle  16347  nndvdslegcd  16542  gcdnncl  16544  divgcdnn  16552  nn0rppwr  16598  sqgcd  16599  eucalgf  16620  eucalginv  16621  lcmgcdlem  16643  lcmftp  16673  lcmfunsnlem2lem1  16675  lcmfunsnlem2lem2  16676  qredeu  16695  rpdvds  16697  cncongr2  16705  divnumden  16785  divdenle  16786  phisum  16828  oddprm  16848  pythagtriplem4  16857  pythagtriplem8  16861  pythagtriplem9  16862  4sqlem10  16985  ram0  17060  cat1lem  18141  isipodrs  18582  gsumval2  18699  smndex1n0mnd  18925  smndex2dnrinv  18928  mulgnn  19093  sylow1lem1  19616  gsumval3eu  19922  ablsimpgfindlem1  20127  ablsimpgfindlem2  20128  ablsimpgfind  20130  fincygsubgodd  20132  rrgnz  20704  fidomndrng  20774  abvtrivd  20833  00lss  20939  lvecvscan2  21114  prmirredlem  21483  uvcff  21811  mvrcl  22012  mplmon  22053  mplmonmul  22054  psdmul  22170  coe1tmfv2  22278  cply1coe0  22305  cply1coe0bi  22306  1marepvsma1  22589  mdetrsca2  22610  mdetrlin2  22613  mdetunilem2  22619  mdetunilem5  22622  mdetunilem6  22623  mdetunilem9  22626  maducoeval2  22646  gsummatr01lem3  22663  gsummatr01lem4  22664  gsummatr01  22665  m2cpm  22747  m2cpminvid2lem  22760  fvmptnn04ifa  22856  fvmptnn04ifb  22857  fvmptnn04ifc  22858  chfacffsupp  22862  chfacfscmul0  22864  chfacfscmulgsum  22866  chfacfpmmul0  22868  chfacfpmmulgsum  22870  connclo  23423  dissnlocfin  23537  ptpjpre2  23588  txindis  23642  snfil  23872  alexsublem  24052  tsmsfbas  24136  stdbdxmet  24528  dscmet  24585  xrsxmet  24831  iccpnfcnv  24975  cphsubrglem  25211  minveclem3b  25462  minveclem4a  25464  ovolicc1  25551  dvexp2  25992  dvmptdiv  26012  lhop2  26054  deg1sublt  26149  ig1pval3  26217  dvply1  26325  plydiveu  26340  quotcan  26351  aaliou3lem9  26392  taylthlem2  26416  taylthlem2OLD  26417  pserdvlem2  26472  abelthlem9  26484  logccne0  26620  logtayllem  26701  logtayl  26702  cxpef  26707  rtprmirr  26803  angrtmuld  26851  isosctrlem3  26863  chordthmlem  26875  leibpilem2  26984  leibpi  26985  rlimcnp2  27009  efrlim  27012  efrlimOLD  27013  vma1  27209  muinv  27236  lgsval2lem  27351  lgsval4  27361  lgsdir  27376  lgseisenlem4  27422  lgsquadlem1  27424  lgsquad2  27430  m1lgs  27432  2sqlem8a  27469  2sqlem8  27470  2sqcoprm  27479  2sqmod  27480  padicabv  27674  ostth1  27677  ostth3  27682  nolesgn2ores  27717  nogesgn1ores  27719  nosep1o  27726  nosep2o  27727  nosepdmlem  27728  nosepssdm  27731  noresle  27742  nosupbnd1lem3  27755  nosupbnd1lem4  27756  nosupbnd1lem5  27757  nosupbnd1lem6  27758  nosupbnd2lem1  27760  noinfbnd1lem3  27770  noinfbnd1lem4  27771  noinfbnd1lem5  27772  noinfbnd1lem6  27773  noinfbnd2lem1  27775  0elold  27947  elnnzs  28387  expsnnval  28409  expsne0  28414  tgbtwnne  28498  tgbtwndiff  28514  tgcolg  28562  tgbtwnconn1lem3  28582  legso  28607  tglineeltr  28639  tglineintmo  28650  tglineneq  28652  colline  28657  mirne  28675  miriso  28678  mirhl  28687  mirbtwnhl  28688  symquadlem  28697  krippenlem  28698  midexlem  28700  ragncol  28717  footexALT  28726  footexlem2  28728  colperp  28737  colperpexlem3  28740  mideulem2  28742  opphllem  28743  midex  28745  opptgdim2  28753  oppperpex  28761  hlpasch  28764  colopp  28777  lmieu  28792  trgcopy  28812  cgracol  28836  cgrg3col4  28861  axlowdimlem15  28971  axcontlem2  28980  axcontlem7  28985  1egrvtxdg0  29529  2pthnloop  29751  cyclnspth  29821  eupth2lem1  30237  eupth2lem2  30238  eupth2lem3lem6  30252  nrt2irr  30492  strlem6  32275  hstrlem6  32283  atssma  32397  chirredlem1  32409  snsssng  32533  ifnetrue  32560  ifnefals  32561  fmptunsnop  32709  xaddeq0  32757  xlt2addrd  32762  fzone1  32802  hashpss  32813  divnumden2  32817  2exple2exp  32834  chnub  33002  submomnd  33087  pmtridf1o  33114  pmtridfv1  33115  pmtridfv2  33116  elrgspnlem2  33247  elrgspnlem3  33248  fracfld  33310  ornglmullt  33337  orngrmullt  33338  ofldchr  33344  suborng  33345  pidlnz  33404  lindssn  33406  drngidl  33461  drngidlhash  33462  0ringprmidl  33477  qsidomlem1  33480  ssdifidlprm  33486  mxidlmaxv  33496  mxidlprm  33498  mxidlirredi  33499  mxidlirred  33500  krull  33507  rsprprmprmidlb  33551  rprmasso2  33554  pidufd  33571  1arithufdlem3  33574  dfufd2  33578  zringidom  33579  0ringmon1p  33583  ig1pnunit  33621  lindsunlem  33675  fldextrspundgdvdslem  33730  fldext2rspun  33732  ply1annnr  33746  fldext2chn  33769  constrextdg2lem  33789  2sqr3minply  33791  1smat1  33803  submatminr1  33809  madjusmdetlem2  33827  zarcls1  33868  zarclsint  33871  zarclssn  33872  xrge0iifcnv  33932  xrge0iifcv  33933  xrge0iif1  33937  qqhval2lem  33982  qqhf  33987  qqhre  34021  esumrnmpt2  34069  esumcvgre  34092  inelpisys  34155  carsgclctunlem2  34321  ballotlemirc  34534  sgnmul  34545  sgn0bi  34550  signswlid  34574  repr0  34626  reprlt  34634  reprgt  34636  reprinfz1  34637  tgoldbachgtda  34676  tgoldbachgt  34678  bnj1523  35085  acycgr2v  35155  fmlaomn0  35395  fmlasucdisj  35404  fz0n  35731  dfrdg2  35796  dfrdg4  35952  broutsideof2  36123  outsidele  36133  rankeq1o  36172  ivthALT  36336  limsucncmpi  36446  topdifinffinlem  37348  icorempo  37352  finxpreclem2  37391  finxp1o  37393  finxpreclem6  37397  poimirlem9  37636  poimirlem11  37638  poimirlem12  37639  poimirlem25  37652  fdc  37752  heibor1lem  37816  heiborlem4  37821  heiborlem6  37823  disjressuc2  38389  2atm  39529  lhpocnle  40018  lhp2at0nle  40037  trlval3  40189  cdleme18c  40295  cdlemg17b  40664  cdlemg17i  40671  dia2dimlem2  41067  dia2dimlem3  41068  dihord6apre  41258  dihatlat  41336  dochshpsat  41456  lcfrlem9  41552  mapdhval2  41728  hdmap1val2  41802  hdmap14lem4a  41873  hdmap14lem6  41875  dvrelogpow2b  42069  aks4d1p1p4  42072  aks4d1p6  42082  fldhmf1  42091  primrootspoweq0  42107  aks6d1c2p2  42120  hashscontpow  42123  aks6d1c5  42140  sticksstones1  42147  sticksstones10  42156  sticksstones12a  42158  sticksstones12  42159  sticksstones22  42169  aks6d1c6lem4  42174  aks6d1c7lem1  42181  aks6d1c7  42185  aks5lem8  42202  metakunt6  42211  metakunt7  42212  metakunt11  42216  metakunt12  42217  metakunt27  42232  metakunt28  42233  metakunt29  42234  metakunt30  42235  negn0nposznnd  42317  mhpind  42604  prjspner1  42636  dffltz  42644  3cubeslem2  42696  jm2.26lem3  43013  kelac1  43075  cantnfresb  43337  tfsconcat0b  43359  nlimsuc  43454  clsk1indlem0  44054  scotteld  44265  sineq0ALT  44957  refsum2cnlem1  45042  disjxp1  45074  nelrnmpt  45089  disjf1  45188  disjrnmpt2  45193  disjinfi  45197  oddfl  45289  xrlttri5d  45295  supxrge  45349  nepnfltpnf  45353  nemnftgtmnft  45355  xrlexaddrp  45363  xrred  45376  supminfxr2  45480  icoiccdif  45537  qinioo  45548  ioonct  45550  fmul01lt1lem1  45599  climrec  45618  limcperiod  45643  reclimc  45668  limsupub  45719  liminflbuz2  45830  cncfiooicclem1  45908  cncfioobdlem  45911  fperdvper  45934  dvdivbd  45938  ditgeqiooicc  45975  itgsincmulx  45989  itgioocnicc  45992  iblcncfioo  45993  stoweidlem35  46050  stoweidlem39  46054  stirlinglem5  46093  stirlinglem8  46096  dirkerper  46111  dirkercncflem2  46119  dirkercncflem4  46121  fourierdlem31  46153  fourierdlem34  46156  fourierdlem41  46163  fourierdlem42  46164  fourierdlem44  46166  fourierdlem48  46169  fourierdlem49  46170  fourierdlem53  46174  fourierdlem56  46177  fourierdlem58  46179  fourierdlem60  46181  fourierdlem61  46182  fourierdlem62  46183  fourierdlem65  46186  fourierdlem66  46187  fourierdlem73  46194  fourierdlem76  46197  fourierdlem79  46200  fourierdlem81  46202  fourierdlem82  46203  fourierdlem93  46214  fourierdlem103  46224  fourierdlem104  46225  sqwvfoura  46243  fourierswlem  46245  elaa2lem  46248  elaa2  46249  etransclem4  46253  etransclem24  46273  etransclem31  46280  etransclem32  46281  etransclem35  46284  sge0repnf  46401  sge0fodjrnlem  46431  sge0iunmpt  46433  sge0rpcpnf  46436  nnfoctbdjlem  46470  meadjun  46477  voliunsge0lem  46487  hoicvr  46563  ovnn0val  46566  ovnsubaddlem1  46585  hoidmvn0val  46599  hsphoidmvle  46601  hoidmv1lelem1  46606  hoidmv1lelem2  46607  hoidmv1lelem3  46608  ovnhoilem1  46616  ovnsubadd2lem  46660  ovnovollem3  46673  lighneallem3  47594  divgcdoddALTV  47669  isubgr0uhgr  47859  usgrexmpl2trifr  47996  gpg5nbgrvtx03star  48036  gpg5nbgr3star  48037  dignn0flhalflem1  48536  itcoval2  48585  itcoval3  48586  itcovalsuc  48588  ackvalsuc1mpt  48599  line2xlem  48674