Theorem neneqd 2942

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1536   ≠ wne 2937

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 2938

This theorem is referenced by:  neneq  2943  necon2bi  2968  necon2i  2972  necon4i  2973  pm2.21ddne  3023  mteqand  3030  nelrdva  3713  eldifsnneq  4795  disjprg  5143  0inp0  5364  rnmptn0  6265  frxp2  8167  frxp3  8174  onnseq  8382  finnzfsuppd  9410  sniffsupp  9437  dfac2b  10168  ackbij1lem15  10270  ttukeylem7  10552  fpwwe2lem12  10679  canthnumlem  10685  canthp1lem2  10690  recgt0  12110  nnneneg  12298  elnnz  12620  xrnemnf  13156  xrnepnf  13157  fzprval  13621  fzodisjsn  13733  expnnval  14101  znsqcld  14198  hashelne0d  14403  elprchashprn2  14431  relexpsucnnr  15060  relexp1g  15061  relexpuzrel  15087  sgnp  15125  fprodn0f  16023  ruclem12  16273  dvdsle  16343  nndvdslegcd  16538  gcdnncl  16540  divgcdnn  16548  nn0rppwr  16594  sqgcd  16595  eucalgf  16616  eucalginv  16617  lcmgcdlem  16639  lcmftp  16669  lcmfunsnlem2lem1  16671  lcmfunsnlem2lem2  16672  qredeu  16691  rpdvds  16693  cncongr2  16701  divnumden  16781  divdenle  16782  phisum  16823  oddprm  16843  pythagtriplem4  16852  pythagtriplem8  16856  pythagtriplem9  16857  4sqlem10  16980  ram0  17055  cat1lem  18149  isipodrs  18594  gsumval2  18711  smndex1n0mnd  18937  smndex2dnrinv  18940  mulgnn  19105  sylow1lem1  19630  gsumval3eu  19936  ablsimpgfindlem1  20141  ablsimpgfindlem2  20142  ablsimpgfind  20144  fincygsubgodd  20146  rrgnz  20720  fidomndrng  20790  abvtrivd  20849  00lss  20956  lvecvscan2  21131  prmirredlem  21500  uvcff  21828  mvrcl  22029  mplmon  22070  mplmonmul  22071  psdmul  22187  coe1tmfv2  22293  cply1coe0  22320  cply1coe0bi  22321  1marepvsma1  22604  mdetrsca2  22625  mdetrlin2  22628  mdetunilem2  22634  mdetunilem5  22637  mdetunilem6  22638  mdetunilem9  22641  maducoeval2  22661  gsummatr01lem3  22678  gsummatr01lem4  22679  gsummatr01  22680  m2cpm  22762  m2cpminvid2lem  22775  fvmptnn04ifa  22871  fvmptnn04ifb  22872  fvmptnn04ifc  22873  chfacffsupp  22877  chfacfscmul0  22879  chfacfscmulgsum  22881  chfacfpmmul0  22883  chfacfpmmulgsum  22885  connclo  23438  dissnlocfin  23552  ptpjpre2  23603  txindis  23657  snfil  23887  alexsublem  24067  tsmsfbas  24151  stdbdxmet  24543  dscmet  24600  xrsxmet  24844  iccpnfcnv  24988  cphsubrglem  25224  minveclem3b  25475  minveclem4a  25477  ovolicc1  25564  dvexp2  26006  dvmptdiv  26026  lhop2  26068  deg1sublt  26163  ig1pval3  26231  dvply1  26339  plydiveu  26354  quotcan  26365  aaliou3lem9  26406  taylthlem2  26430  taylthlem2OLD  26431  pserdvlem2  26486  abelthlem9  26498  logccne0  26634  logtayllem  26715  logtayl  26716  cxpef  26721  rtprmirr  26817  angrtmuld  26865  isosctrlem3  26877  chordthmlem  26889  leibpilem2  26998  leibpi  26999  rlimcnp2  27023  efrlim  27026  efrlimOLD  27027  vma1  27223  muinv  27250  lgsval2lem  27365  lgsval4  27375  lgsdir  27390  lgseisenlem4  27436  lgsquadlem1  27438  lgsquad2  27444  m1lgs  27446  2sqlem8a  27483  2sqlem8  27484  2sqcoprm  27493  2sqmod  27494  padicabv  27688  ostth1  27691  ostth3  27696  nolesgn2ores  27731  nogesgn1ores  27733  nosep1o  27740  nosep2o  27741  nosepdmlem  27742  nosepssdm  27745  noresle  27756  nosupbnd1lem3  27769  nosupbnd1lem4  27770  nosupbnd1lem5  27771  nosupbnd1lem6  27772  nosupbnd2lem1  27774  noinfbnd1lem3  27784  noinfbnd1lem4  27785  noinfbnd1lem5  27786  noinfbnd1lem6  27787  noinfbnd2lem1  27789  0elold  27961  elnnzs  28401  expsnnval  28423  expsne0  28428  tgbtwnne  28512  tgbtwndiff  28528  tgcolg  28576  tgbtwnconn1lem3  28596  legso  28621  tglineeltr  28653  tglineintmo  28664  tglineneq  28666  colline  28671  mirne  28689  miriso  28692  mirhl  28701  mirbtwnhl  28702  symquadlem  28711  krippenlem  28712  midexlem  28714  ragncol  28731  footexALT  28740  footexlem2  28742  colperp  28751  colperpexlem3  28754  mideulem2  28756  opphllem  28757  midex  28759  opptgdim2  28767  oppperpex  28775  hlpasch  28778  colopp  28791  lmieu  28806  trgcopy  28826  cgracol  28850  cgrg3col4  28875  axlowdimlem15  28985  axcontlem2  28994  axcontlem7  28999  1egrvtxdg0  29543  2pthnloop  29763  cyclnspth  29832  eupth2lem1  30246  eupth2lem2  30247  eupth2lem3lem6  30261  nrt2irr  30501  strlem6  32284  hstrlem6  32292  atssma  32406  chirredlem1  32418  snsssng  32541  ifnetrue  32567  ifnefals  32568  fmptunsnop  32714  xaddeq0  32763  xlt2addrd  32768  fzone1  32807  divnumden2  32821  chnub  32985  submomnd  33069  pmtridf1o  33096  pmtridfv1  33097  pmtridfv2  33098  elrgspnlem2  33232  elrgspnlem3  33233  fracfld  33289  ornglmullt  33316  orngrmullt  33317  ofldchr  33323  suborng  33324  pidlnz  33383  lindssn  33385  drngidl  33440  drngidlhash  33441  0ringprmidl  33456  qsidomlem1  33459  ssdifidlprm  33465  mxidlmaxv  33475  mxidlprm  33477  mxidlirredi  33478  mxidlirred  33479  krull  33486  rsprprmprmidlb  33530  rprmasso2  33533  pidufd  33550  1arithufdlem3  33553  dfufd2  33557  zringidom  33558  0ringmon1p  33562  ig1pnunit  33600  lindsunlem  33651  ply1annnr  33710  fldext2chn  33733  2sqr3minply  33752  1smat1  33764  submatminr1  33770  madjusmdetlem2  33788  zarcls1  33829  zarclsint  33832  zarclssn  33833  xrge0iifcnv  33893  xrge0iifcv  33894  xrge0iif1  33898  qqhval2lem  33943  qqhf  33948  qqhre  33982  esumrnmpt2  34048  esumcvgre  34071  inelpisys  34134  carsgclctunlem2  34300  ballotlemirc  34512  sgnmul  34523  sgn0bi  34528  signswlid  34552  repr0  34604  reprlt  34612  reprgt  34614  reprinfz1  34615  tgoldbachgtda  34654  tgoldbachgt  34656  bnj1523  35063  acycgr2v  35134  fmlaomn0  35374  fmlasucdisj  35383  fz0n  35710  dfrdg2  35776  dfrdg4  35932  broutsideof2  36103  outsidele  36113  rankeq1o  36152  ivthALT  36317  limsucncmpi  36427  topdifinffinlem  37329  icorempo  37333  finxpreclem2  37372  finxp1o  37374  finxpreclem6  37378  poimirlem9  37615  poimirlem11  37617  poimirlem12  37618  poimirlem25  37631  fdc  37731  heibor1lem  37795  heiborlem4  37800  heiborlem6  37802  disjressuc2  38369  2atm  39509  lhpocnle  39998  lhp2at0nle  40017  trlval3  40169  cdleme18c  40275  cdlemg17b  40644  cdlemg17i  40651  dia2dimlem2  41047  dia2dimlem3  41048  dihord6apre  41238  dihatlat  41316  dochshpsat  41436  lcfrlem9  41532  mapdhval2  41708  hdmap1val2  41782  hdmap14lem4a  41853  hdmap14lem6  41855  dvrelogpow2b  42049  aks4d1p1p4  42052  aks4d1p6  42062  fldhmf1  42071  primrootspoweq0  42087  aks6d1c2p2  42100  hashscontpow  42103  aks6d1c5  42120  sticksstones1  42127  sticksstones10  42136  sticksstones12a  42138  sticksstones12  42139  sticksstones22  42149  aks6d1c6lem4  42154  aks6d1c7lem1  42161  aks6d1c7  42165  aks5lem8  42182  metakunt6  42191  metakunt7  42192  metakunt11  42196  metakunt12  42197  metakunt27  42212  metakunt28  42213  metakunt29  42214  metakunt30  42215  negn0nposznnd  42295  mhpind  42580  prjspner1  42612  dffltz  42620  3cubeslem2  42672  jm2.26lem3  42989  kelac1  43051  cantnfresb  43313  tfsconcat0b  43335  nlimsuc  43430  clsk1indlem0  44030  scotteld  44241  sineq0ALT  44934  refsum2cnlem1  44974  disjxp1  45008  nelrnmpt  45023  disjf1  45125  disjrnmpt2  45130  disjinfi  45134  oddfl  45227  xrlttri5d  45233  supxrge  45287  nepnfltpnf  45291  nemnftgtmnft  45293  xrlexaddrp  45301  xrred  45314  supminfxr2  45418  icoiccdif  45476  qinioo  45487  ioonct  45489  fmul01lt1lem1  45539  climrec  45558  limcperiod  45583  reclimc  45608  limsupub  45659  liminflbuz2  45770  cncfiooicclem1  45848  cncfioobdlem  45851  fperdvper  45874  dvdivbd  45878  ditgeqiooicc  45915  itgsincmulx  45929  itgioocnicc  45932  iblcncfioo  45933  stoweidlem35  45990  stoweidlem39  45994  stirlinglem5  46033  stirlinglem8  46036  dirkerper  46051  dirkercncflem2  46059  dirkercncflem4  46061  fourierdlem31  46093  fourierdlem34  46096  fourierdlem41  46103  fourierdlem42  46104  fourierdlem44  46106  fourierdlem48  46109  fourierdlem49  46110  fourierdlem53  46114  fourierdlem56  46117  fourierdlem58  46119  fourierdlem60  46121  fourierdlem61  46122  fourierdlem62  46123  fourierdlem65  46126  fourierdlem66  46127  fourierdlem73  46134  fourierdlem76  46137  fourierdlem79  46140  fourierdlem81  46142  fourierdlem82  46143  fourierdlem93  46154  fourierdlem103  46164  fourierdlem104  46165  sqwvfoura  46183  fourierswlem  46185  elaa2lem  46188  elaa2  46189  etransclem4  46193  etransclem24  46213  etransclem31  46220  etransclem32  46221  etransclem35  46224  sge0repnf  46341  sge0fodjrnlem  46371  sge0iunmpt  46373  sge0rpcpnf  46376  nnfoctbdjlem  46410  meadjun  46417  voliunsge0lem  46427  hoicvr  46503  ovnn0val  46506  ovnsubaddlem1  46525  hoidmvn0val  46539  hsphoidmvle  46541  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1lelem3  46548  ovnhoilem1  46556  ovnsubadd2lem  46600  ovnovollem3  46613  lighneallem3  47531  divgcdoddALTV  47606  isubgr0uhgr  47796  usgrexmpl2trifr  47931  gpg5nbgrvtx03star  47970  gpg5nbgr3star  47971  dignn0flhalflem1  48464  itcoval2  48513  itcoval3  48514  itcovalsuc  48516  ackvalsuc1mpt  48527  line2xlem  48602