Theorem neneqd 2937

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

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

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 2933

This theorem is referenced by:  neneq  2938  necon2bi  2962  necon2i  2966  necon4i  2967  pm2.21ddne  3016  mteqand  3023  nelrdva  3688  eldifsnneq  4767  disjprg  5115  0inp0  5329  rnmptn0  6233  resf1extb  7928  frxp2  8141  frxp3  8148  onnseq  8356  finnzfsuppd  9383  sniffsupp  9410  dfac2b  10143  ackbij1lem15  10245  ttukeylem7  10527  fpwwe2lem12  10654  canthnumlem  10660  canthp1lem2  10665  recgt0  12085  nnneneg  12273  elnnz  12596  xrnemnf  13131  xrnepnf  13132  fzprval  13600  fzodisjsn  13712  expnnval  14080  znsqcld  14178  hashelne0d  14384  elprchashprn2  14412  relexpsucnnr  15042  relexp1g  15043  relexpuzrel  15069  sgnp  15107  fprodn0f  16005  ruclem12  16257  dvdsle  16327  nndvdslegcd  16522  gcdnncl  16524  divgcdnn  16532  nn0rppwr  16578  sqgcd  16579  eucalgf  16600  eucalginv  16601  lcmgcdlem  16623  lcmftp  16653  lcmfunsnlem2lem1  16655  lcmfunsnlem2lem2  16656  qredeu  16675  rpdvds  16677  cncongr2  16685  divnumden  16765  divdenle  16766  phisum  16808  oddprm  16828  pythagtriplem4  16837  pythagtriplem8  16841  pythagtriplem9  16842  4sqlem10  16965  ram0  17040  cat1lem  18107  isipodrs  18545  gsumval2  18662  smndex1n0mnd  18888  smndex2dnrinv  18891  mulgnn  19056  sylow1lem1  19577  gsumval3eu  19883  ablsimpgfindlem1  20088  ablsimpgfindlem2  20089  ablsimpgfind  20091  fincygsubgodd  20093  rrgnz  20662  fidomndrng  20731  abvtrivd  20790  00lss  20896  lvecvscan2  21071  prmirredlem  21431  uvcff  21749  mvrcl  21950  mplmon  21991  mplmonmul  21992  psdmul  22102  coe1tmfv2  22210  cply1coe0  22237  cply1coe0bi  22238  1marepvsma1  22519  mdetrsca2  22540  mdetrlin2  22543  mdetunilem2  22549  mdetunilem5  22552  mdetunilem6  22553  mdetunilem9  22556  maducoeval2  22576  gsummatr01lem3  22593  gsummatr01lem4  22594  gsummatr01  22595  m2cpm  22677  m2cpminvid2lem  22690  fvmptnn04ifa  22786  fvmptnn04ifb  22787  fvmptnn04ifc  22788  chfacffsupp  22792  chfacfscmul0  22794  chfacfscmulgsum  22796  chfacfpmmul0  22798  chfacfpmmulgsum  22800  connclo  23351  dissnlocfin  23465  ptpjpre2  23516  txindis  23570  snfil  23800  alexsublem  23980  tsmsfbas  24064  stdbdxmet  24452  dscmet  24509  xrsxmet  24747  iccpnfcnv  24891  cphsubrglem  25127  minveclem3b  25378  minveclem4a  25380  ovolicc1  25467  dvexp2  25908  dvmptdiv  25928  lhop2  25970  deg1sublt  26065  ig1pval3  26133  dvply1  26241  plydiveu  26256  quotcan  26267  aaliou3lem9  26308  taylthlem2  26332  taylthlem2OLD  26333  pserdvlem2  26388  abelthlem9  26400  logccne0  26537  logtayllem  26618  logtayl  26619  cxpef  26624  rtprmirr  26720  angrtmuld  26768  isosctrlem3  26780  chordthmlem  26792  leibpilem2  26901  leibpi  26902  rlimcnp2  26926  efrlim  26929  efrlimOLD  26930  vma1  27126  muinv  27153  lgsval2lem  27268  lgsval4  27278  lgsdir  27293  lgseisenlem4  27339  lgsquadlem1  27341  lgsquad2  27347  m1lgs  27349  2sqlem8a  27386  2sqlem8  27387  2sqcoprm  27396  2sqmod  27397  padicabv  27591  ostth1  27594  ostth3  27599  nolesgn2ores  27634  nogesgn1ores  27636  nosep1o  27643  nosep2o  27644  nosepdmlem  27645  nosepssdm  27648  noresle  27659  nosupbnd1lem3  27672  nosupbnd1lem4  27673  nosupbnd1lem5  27674  nosupbnd1lem6  27675  nosupbnd2lem1  27677  noinfbnd1lem3  27687  noinfbnd1lem4  27688  noinfbnd1lem5  27689  noinfbnd1lem6  27690  noinfbnd2lem1  27692  0elold  27864  elnnzs  28304  expsnnval  28326  expsne0  28331  tgbtwnne  28415  tgbtwndiff  28431  tgcolg  28479  tgbtwnconn1lem3  28499  legso  28524  tglineeltr  28556  tglineintmo  28567  tglineneq  28569  colline  28574  mirne  28592  miriso  28595  mirhl  28604  mirbtwnhl  28605  symquadlem  28614  krippenlem  28615  midexlem  28617  ragncol  28634  footexALT  28643  footexlem2  28645  colperp  28654  colperpexlem3  28657  mideulem2  28659  opphllem  28660  midex  28662  opptgdim2  28670  oppperpex  28678  hlpasch  28681  colopp  28694  lmieu  28709  trgcopy  28729  cgracol  28753  cgrg3col4  28778  axlowdimlem15  28881  axcontlem2  28890  axcontlem7  28895  1egrvtxdg0  29437  2pthnloop  29659  cyclnspth  29729  eupth2lem1  30145  eupth2lem2  30146  eupth2lem3lem6  30160  nrt2irr  30400  strlem6  32183  hstrlem6  32191  atssma  32305  chirredlem1  32317  snsssng  32441  ifnetrue  32474  ifnefals  32475  fmptunsnop  32623  xaddeq0  32676  rexmul2  32677  xlt2addrd  32682  xnn0nn0d  32695  fzone1  32723  hashpss  32734  elq2  32736  divnumden2  32740  sgnmul  32760  sgn0bi  32765  2exple2exp  32770  chnub  32938  submomnd  33024  pmtridf1o  33051  pmtridfv1  33052  pmtridfv2  33053  elrgspnlem2  33184  elrgspnlem3  33185  fracfld  33248  ornglmullt  33275  orngrmullt  33276  ofldchr  33282  suborng  33283  pidlnz  33337  lindssn  33339  drngidl  33394  drngidlhash  33395  0ringprmidl  33410  qsidomlem1  33413  ssdifidlprm  33419  mxidlmaxv  33429  mxidlprm  33431  mxidlirredi  33432  mxidlirred  33433  krull  33440  rsprprmprmidlb  33484  rprmasso2  33487  pidufd  33504  1arithufdlem3  33507  dfufd2  33511  zringidom  33512  0ringmon1p  33516  ig1pnunit  33556  lindsunlem  33610  fldextrspundgdvdslem  33667  fldext2rspun  33669  ply1annnr  33683  fldext2chn  33708  constrextdg2lem  33728  constrext2chnlem  33730  constrcon  33754  2sqr3minply  33760  cos9thpiminply  33768  1smat1  33781  submatminr1  33787  madjusmdetlem2  33805  zarcls1  33846  zarclsint  33849  zarclssn  33850  xrge0iifcnv  33910  xrge0iifcv  33911  xrge0iif1  33915  qqhval2lem  33958  qqhf  33963  qqhre  33997  esumrnmpt2  34045  esumcvgre  34068  inelpisys  34131  carsgclctunlem2  34297  ballotlemirc  34510  signswlid  34537  repr0  34589  reprlt  34597  reprgt  34599  reprinfz1  34600  tgoldbachgtda  34639  tgoldbachgt  34641  bnj1523  35048  acycgr2v  35118  fmlaomn0  35358  fmlasucdisj  35367  fz0n  35694  dfrdg2  35759  dfrdg4  35915  broutsideof2  36086  outsidele  36096  rankeq1o  36135  ivthALT  36299  limsucncmpi  36409  topdifinffinlem  37311  icorempo  37315  finxpreclem2  37354  finxp1o  37356  finxpreclem6  37360  poimirlem9  37599  poimirlem11  37601  poimirlem12  37602  poimirlem25  37615  fdc  37715  heibor1lem  37779  heiborlem4  37784  heiborlem6  37786  disjressuc2  38352  2atm  39492  lhpocnle  39981  lhp2at0nle  40000  trlval3  40152  cdleme18c  40258  cdlemg17b  40627  cdlemg17i  40634  dia2dimlem2  41030  dia2dimlem3  41031  dihord6apre  41221  dihatlat  41299  dochshpsat  41419  lcfrlem9  41515  mapdhval2  41691  hdmap1val2  41765  hdmap14lem4a  41836  hdmap14lem6  41838  dvrelogpow2b  42027  aks4d1p1p4  42030  aks4d1p6  42040  fldhmf1  42049  primrootspoweq0  42065  aks6d1c2p2  42078  hashscontpow  42081  aks6d1c5  42098  sticksstones1  42105  sticksstones10  42114  sticksstones12a  42116  sticksstones12  42117  sticksstones22  42127  aks6d1c6lem4  42132  aks6d1c7lem1  42139  aks6d1c7  42143  aks5lem8  42160  metakunt6  42169  metakunt7  42170  metakunt11  42174  metakunt12  42175  metakunt27  42190  metakunt28  42191  metakunt29  42192  metakunt30  42193  negn0nposznnd  42279  mhpind  42564  prjspner1  42596  dffltz  42604  3cubeslem2  42655  jm2.26lem3  42972  kelac1  43034  cantnfresb  43295  tfsconcat0b  43317  nlimsuc  43412  clsk1indlem0  44012  scotteld  44218  sineq0ALT  44909  refsum2cnlem1  45009  disjxp1  45041  nelrnmpt  45056  disjf1  45155  disjrnmpt2  45160  disjinfi  45164  oddfl  45254  xrlttri5d  45260  supxrge  45313  nepnfltpnf  45317  nemnftgtmnft  45319  xrlexaddrp  45327  xrred  45340  supminfxr2  45444  icoiccdif  45501  qinioo  45512  ioonct  45514  fmul01lt1lem1  45561  climrec  45580  limcperiod  45605  reclimc  45630  limsupub  45681  liminflbuz2  45792  cncfiooicclem1  45870  cncfioobdlem  45873  fperdvper  45896  dvdivbd  45900  ditgeqiooicc  45937  itgsincmulx  45951  itgioocnicc  45954  iblcncfioo  45955  stoweidlem35  46012  stoweidlem39  46016  stirlinglem5  46055  stirlinglem8  46058  dirkerper  46073  dirkercncflem2  46081  dirkercncflem4  46083  fourierdlem31  46115  fourierdlem34  46118  fourierdlem41  46125  fourierdlem42  46126  fourierdlem44  46128  fourierdlem48  46131  fourierdlem49  46132  fourierdlem53  46136  fourierdlem56  46139  fourierdlem58  46141  fourierdlem60  46143  fourierdlem61  46144  fourierdlem62  46145  fourierdlem65  46148  fourierdlem66  46149  fourierdlem73  46156  fourierdlem76  46159  fourierdlem79  46162  fourierdlem81  46164  fourierdlem82  46165  fourierdlem93  46176  fourierdlem103  46186  fourierdlem104  46187  sqwvfoura  46205  fourierswlem  46207  elaa2lem  46210  elaa2  46211  etransclem4  46215  etransclem24  46235  etransclem31  46242  etransclem32  46243  etransclem35  46246  sge0repnf  46363  sge0fodjrnlem  46393  sge0iunmpt  46395  sge0rpcpnf  46398  nnfoctbdjlem  46432  meadjun  46439  voliunsge0lem  46449  hoicvr  46525  ovnn0val  46528  ovnsubaddlem1  46547  hoidmvn0val  46561  hsphoidmvle  46563  hoidmv1lelem1  46568  hoidmv1lelem2  46569  hoidmv1lelem3  46570  ovnhoilem1  46578  ovnsubadd2lem  46622  ovnovollem3  46635  lighneallem3  47569  divgcdoddALTV  47644  isubgr0uhgr  47834  usgrexmpl2trifr  47989  gpg5nbgrvtx03star  48030  gpg5nbgr3star  48031  dignn0flhalflem1  48543  itcoval2  48592  itcoval3  48593  itcovalsuc  48595  ackvalsuc1mpt  48606  line2xlem  48681