Theorem neneqd 2946

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2941

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 206  df-ne 2942

This theorem is referenced by:  neneq  2947  necon2bi  2972  necon2i  2976  necon4i  2977  pm2.21ddne  3027  mteqand  3034  nelrdva  3701  eldifsnneq  4794  disjprg  5144  0inp0  5357  rnmptn0  6241  frxp2  8127  frxp3  8134  onnseq  8341  sniffsupp  9392  dfac2b  10122  ackbij1lem15  10226  ttukeylem7  10507  fpwwe2lem12  10634  canthnumlem  10640  canthp1lem2  10645  recgt0  12057  nnneneg  12244  elnnz  12565  xrnemnf  13094  xrnepnf  13095  fzprval  13559  fzodisjsn  13667  expnnval  14027  znsqcld  14124  hashelne0d  14325  elprchashprn2  14353  relexpsucnnr  14969  relexp1g  14970  relexpuzrel  14996  sgnp  15034  fprodn0f  15932  ruclem12  16181  dvdsle  16250  nndvdslegcd  16443  gcdnncl  16445  divgcdnn  16453  sqgcd  16499  eucalgf  16517  eucalginv  16518  lcmgcdlem  16540  lcmftp  16570  lcmfunsnlem2lem1  16572  lcmfunsnlem2lem2  16573  qredeu  16592  rpdvds  16594  cncongr2  16602  divnumden  16681  divdenle  16682  phisum  16720  oddprm  16740  pythagtriplem4  16749  pythagtriplem8  16753  pythagtriplem9  16754  4sqlem10  16877  ram0  16952  cat1lem  18043  isipodrs  18487  gsumval2  18602  smndex1n0mnd  18790  smndex2dnrinv  18793  mulgnn  18953  sylow1lem1  19461  gsumval3eu  19767  ablsimpgfindlem1  19972  ablsimpgfindlem2  19973  ablsimpgfind  19975  fincygsubgodd  19977  abvtrivd  20441  00lss  20545  lvecvscan2  20718  fidomndrng  20919  prmirredlem  21034  uvcff  21338  mvrcl  21543  mplmon  21582  mplmonmul  21583  coe1tmfv2  21789  cply1coe0  21815  cply1coe0bi  21816  1marepvsma1  22077  mdetrsca2  22098  mdetrlin2  22101  mdetunilem2  22107  mdetunilem5  22110  mdetunilem6  22111  mdetunilem9  22114  maducoeval2  22134  gsummatr01lem3  22151  gsummatr01lem4  22152  gsummatr01  22153  m2cpm  22235  m2cpminvid2lem  22248  fvmptnn04ifa  22344  fvmptnn04ifb  22345  fvmptnn04ifc  22346  chfacffsupp  22350  chfacfscmul0  22352  chfacfscmulgsum  22354  chfacfpmmul0  22356  chfacfpmmulgsum  22358  connclo  22911  dissnlocfin  23025  ptpjpre2  23076  txindis  23130  snfil  23360  alexsublem  23540  tsmsfbas  23624  stdbdxmet  24016  dscmet  24073  xrsxmet  24317  iccpnfcnv  24452  cphsubrglem  24686  minveclem3b  24937  minveclem4a  24939  ovolicc1  25025  dvexp2  25463  dvmptdiv  25483  lhop2  25524  deg1sublt  25620  ig1pval3  25684  dvply1  25789  plydiveu  25803  quotcan  25814  aaliou3lem9  25855  taylthlem2  25878  pserdvlem2  25932  abelthlem9  25944  logccne0  26079  logtayllem  26159  logtayl  26160  cxpef  26165  angrtmuld  26303  isosctrlem3  26315  chordthmlem  26327  leibpilem2  26436  leibpi  26437  rlimcnp2  26461  efrlim  26464  vma1  26660  muinv  26687  lgsval2lem  26800  lgsval4  26810  lgsdir  26825  lgseisenlem4  26871  lgsquadlem1  26873  lgsquad2  26879  m1lgs  26881  2sqlem8a  26918  2sqlem8  26919  2sqcoprm  26928  2sqmod  26929  padicabv  27123  ostth1  27126  ostth3  27131  nolesgn2ores  27165  nogesgn1ores  27167  nosep1o  27174  nosep2o  27175  nosepdmlem  27176  nosepssdm  27179  noresle  27190  nosupbnd1lem3  27203  nosupbnd1lem4  27204  nosupbnd1lem5  27205  nosupbnd1lem6  27206  nosupbnd2lem1  27208  noinfbnd1lem3  27218  noinfbnd1lem4  27219  noinfbnd1lem5  27220  noinfbnd1lem6  27221  noinfbnd2lem1  27223  0elold  27392  tgbtwnne  27731  tgbtwndiff  27747  tgcolg  27795  tgbtwnconn1lem3  27815  legso  27840  tglineeltr  27872  tglineintmo  27883  tglineneq  27885  colline  27890  mirne  27908  miriso  27911  mirhl  27920  mirbtwnhl  27921  symquadlem  27930  krippenlem  27931  midexlem  27933  ragncol  27950  footexALT  27959  footexlem2  27961  colperp  27970  colperpexlem3  27973  mideulem2  27975  opphllem  27976  midex  27978  opptgdim2  27986  oppperpex  27994  hlpasch  27997  colopp  28010  lmieu  28025  trgcopy  28045  cgracol  28069  cgrg3col4  28094  axlowdimlem15  28204  axcontlem2  28213  axcontlem7  28218  1egrvtxdg0  28758  2pthnloop  28978  cyclnspth  29047  eupth2lem1  29461  eupth2lem2  29462  eupth2lem3lem6  29476  strlem6  31497  hstrlem6  31505  atssma  31619  chirredlem1  31631  snsssng  31740  ifnetrue  31767  ifnefals  31768  xaddeq0  31954  xlt2addrd  31959  fzone1  31999  divnumden2  32012  submomnd  32216  pmtridf1o  32241  pmtridfv1  32242  pmtridfv2  32243  ornglmullt  32414  orngrmullt  32415  ofldchr  32421  suborng  32422  pidlnz  32477  lindssn  32483  drngidl  32540  drngidlhash  32541  0ringprmidl  32557  qsidomlem1  32560  mxidlmaxv  32573  mxidlprm  32575  mxidlirredi  32576  mxidlirred  32577  krull  32583  0ringmon1p  32625  ig1pnunit  32659  lindsunlem  32698  ply1annnr  32753  1smat1  32773  submatminr1  32779  madjusmdetlem2  32797  zarcls1  32838  zarclsint  32841  zarclssn  32842  xrge0iifcnv  32902  xrge0iifcv  32903  xrge0iif1  32907  qqhval2lem  32950  qqhf  32955  qqhre  32989  esumrnmpt2  33055  esumcvgre  33078  inelpisys  33141  carsgclctunlem2  33307  ballotlemirc  33519  sgnmul  33530  sgn0bi  33535  signswlid  33559  repr0  33612  reprlt  33620  reprgt  33622  reprinfz1  33623  tgoldbachgtda  33662  tgoldbachgt  33664  bnj1523  34071  acycgr2v  34130  fmlaomn0  34370  fmlasucdisj  34379  fz0n  34689  dfrdg2  34756  dfrdg4  34912  broutsideof2  35083  outsidele  35093  rankeq1o  35132  ivthALT  35209  limsucncmpi  35319  topdifinffinlem  36217  icorempo  36221  finxpreclem2  36260  finxp1o  36262  finxpreclem6  36266  poimirlem9  36486  poimirlem11  36488  poimirlem12  36489  poimirlem25  36502  fdc  36602  heibor1lem  36666  heiborlem4  36671  heiborlem6  36673  disjressuc2  37247  2atm  38387  lhpocnle  38876  lhp2at0nle  38895  trlval3  39047  cdleme18c  39153  cdlemg17b  39522  cdlemg17i  39529  dia2dimlem2  39925  dia2dimlem3  39926  dihord6apre  40116  dihatlat  40194  dochshpsat  40314  lcfrlem9  40410  mapdhval2  40586  hdmap1val2  40660  hdmap14lem4a  40731  hdmap14lem6  40733  dvrelogpow2b  40922  aks4d1p1p4  40925  aks4d1p6  40935  fldhmf1  40944  aks6d1c2p2  40946  sticksstones1  40951  sticksstones10  40960  sticksstones12a  40962  sticksstones12  40963  sticksstones22  40973  metakunt6  40979  metakunt7  40980  metakunt11  40984  metakunt12  40985  metakunt27  41000  metakunt28  41001  metakunt29  41002  metakunt30  41003  mhpind  41164  negn0nposznnd  41192  nn0rppwr  41220  rtprmirr  41234  prjspner1  41365  dffltz  41373  3cubeslem2  41409  jm2.26lem3  41726  kelac1  41791  cantnfresb  42060  tfsconcat0b  42082  nlimsuc  42178  clsk1indlem0  42778  finnzfsuppd  42947  scotteld  42991  sineq0ALT  43684  refsum2cnlem1  43707  disjxp1  43742  nelrnmpt  43759  disjf1  43866  disjrnmpt2  43872  disjinfi  43877  oddfl  43974  xrlttri5d  43980  supxrge  44035  nepnfltpnf  44039  nemnftgtmnft  44041  xrlexaddrp  44049  xrred  44062  supminfxr2  44166  icoiccdif  44224  qinioo  44235  ioonct  44237  fmul01lt1lem1  44287  climrec  44306  limcperiod  44331  reclimc  44356  limsupub  44407  liminflbuz2  44518  cncfiooicclem1  44596  cncfioobdlem  44599  fperdvper  44622  dvdivbd  44626  ditgeqiooicc  44663  itgsincmulx  44677  itgioocnicc  44680  iblcncfioo  44681  stoweidlem35  44738  stoweidlem39  44742  stirlinglem5  44781  stirlinglem8  44784  dirkerper  44799  dirkercncflem2  44807  dirkercncflem4  44809  fourierdlem31  44841  fourierdlem34  44844  fourierdlem41  44851  fourierdlem42  44852  fourierdlem44  44854  fourierdlem48  44857  fourierdlem49  44858  fourierdlem53  44862  fourierdlem56  44865  fourierdlem58  44867  fourierdlem60  44869  fourierdlem61  44870  fourierdlem62  44871  fourierdlem65  44874  fourierdlem66  44875  fourierdlem73  44882  fourierdlem76  44885  fourierdlem79  44888  fourierdlem81  44890  fourierdlem82  44891  fourierdlem93  44902  fourierdlem103  44912  fourierdlem104  44913  sqwvfoura  44931  fourierswlem  44933  elaa2lem  44936  elaa2  44937  etransclem4  44941  etransclem24  44961  etransclem31  44968  etransclem32  44969  etransclem35  44972  sge0repnf  45089  sge0fodjrnlem  45119  sge0iunmpt  45121  sge0rpcpnf  45124  nnfoctbdjlem  45158  meadjun  45165  voliunsge0lem  45175  hoicvr  45251  ovnn0val  45254  ovnsubaddlem1  45273  hoidmvn0val  45287  hsphoidmvle  45289  hoidmv1lelem1  45294  hoidmv1lelem2  45295  hoidmv1lelem3  45296  ovnhoilem1  45304  ovnsubadd2lem  45348  ovnovollem3  45361  lighneallem3  46262  divgcdoddALTV  46337  dignn0flhalflem1  47255  itcoval2  47304  itcoval3  47305  itcovalsuc  47307  ackvalsuc1mpt  47318  line2xlem  47393