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 1542   ≠ 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  3651  eldifsnneq  4736  disjprg  5081  0inp0  5300  nelrnmpt  5922  rnmptn0  6208  resf1extb  7885  frxp2  8094  frxp3  8101  onnseq  8284  finnzfsuppd  9286  sniffsupp  9313  dfac2b  10053  ackbij1lem15  10155  ttukeylem7  10437  fpwwe2lem12  10565  canthnumlem  10571  canthp1lem2  10576  recgt0  12001  nnneneg  12212  elnnz  12534  xrnemnf  13068  xrnepnf  13069  fzprval  13539  fzodisjsn  13652  fzone1  13739  expnnval  14026  znsqcld  14124  hashelne0d  14330  elprchashprn2  14358  relexpsucnnr  14987  relexp1g  14988  relexpuzrel  15014  sgnp  15052  fprodn0f  15956  ruclem12  16208  dvdsle  16279  nndvdslegcd  16474  gcdnncl  16476  divgcdnn  16484  nn0rppwr  16530  sqgcd  16531  eucalgf  16552  eucalginv  16553  lcmgcdlem  16575  lcmftp  16605  lcmfunsnlem2lem1  16607  lcmfunsnlem2lem2  16608  qredeu  16627  rpdvds  16629  cncongr2  16637  divnumden  16718  divdenle  16719  phisum  16761  oddprm  16781  pythagtriplem4  16790  pythagtriplem8  16794  pythagtriplem9  16795  4sqlem10  16918  ram0  16993  cat1lem  18063  isipodrs  18503  chnub  18588  chnpof1  18596  gsumval2  18654  smndex1n0mnd  18883  smndex2dnrinv  18886  mulgnn  19051  sylow1lem1  19573  gsumval3eu  19879  ablsimpgfindlem1  20084  ablsimpgfindlem2  20085  ablsimpgfind  20087  fincygsubgodd  20089  submomnd  20107  rrgnz  20681  fidomndrng  20750  abvtrivd  20809  ornglmullt  20846  orngrmullt  20847  suborng  20853  00lss  20936  lvecvscan2  21110  prmirredlem  21452  ofldchr  21556  uvcff  21771  mvrcl  21970  mplmon  22013  mplmonmul  22014  psdmul  22132  coe1tmfv2  22240  cply1coe0  22266  cply1coe0bi  22267  1marepvsma1  22548  mdetrsca2  22569  mdetrlin2  22572  mdetunilem2  22578  mdetunilem5  22581  mdetunilem6  22582  mdetunilem9  22585  maducoeval2  22605  gsummatr01lem3  22622  gsummatr01lem4  22623  gsummatr01  22624  m2cpm  22706  m2cpminvid2lem  22719  fvmptnn04ifa  22815  fvmptnn04ifb  22816  fvmptnn04ifc  22817  chfacffsupp  22821  chfacfscmul0  22823  chfacfscmulgsum  22825  chfacfpmmul0  22827  chfacfpmmulgsum  22829  connclo  23380  dissnlocfin  23494  ptpjpre2  23545  txindis  23599  snfil  23829  alexsublem  24009  tsmsfbas  24093  stdbdxmet  24480  dscmet  24537  xrsxmet  24775  iccpnfcnv  24911  cphsubrglem  25144  minveclem3b  25395  minveclem4a  25397  ovolicc1  25483  dvexp2  25921  dvmptdiv  25941  lhop2  25982  deg1sublt  26075  ig1pval3  26143  dvply1  26250  plydiveu  26264  quotcan  26275  aaliou3lem9  26316  taylthlem2  26339  pserdvlem2  26393  abelthlem9  26405  logccne0  26542  logtayllem  26623  logtayl  26624  cxpef  26629  rtprmirr  26724  angrtmuld  26772  isosctrlem3  26784  chordthmlem  26796  leibpilem2  26905  leibpi  26906  rlimcnp2  26930  efrlim  26933  vma1  27129  muinv  27156  lgsval2lem  27270  lgsval4  27280  lgsdir  27295  lgseisenlem4  27341  lgsquadlem1  27343  lgsquad2  27349  m1lgs  27351  2sqlem8a  27388  2sqlem8  27389  2sqcoprm  27398  2sqmod  27399  padicabv  27593  ostth1  27596  ostth3  27601  nolesgn2ores  27636  nogesgn1ores  27638  nosep1o  27645  nosep2o  27646  nosepdmlem  27647  nosepssdm  27650  noresle  27661  nosupbnd1lem3  27674  nosupbnd1lem4  27675  nosupbnd1lem5  27676  nosupbnd1lem6  27677  nosupbnd2lem1  27679  noinfbnd1lem3  27689  noinfbnd1lem4  27690  noinfbnd1lem5  27691  noinfbnd1lem6  27692  noinfbnd2lem1  27694  0elold  27902  elnnzs  28393  expnnsval  28418  expsne0  28428  bdayfinbndlem1  28459  tgbtwnne  28558  tgbtwndiff  28574  tgcolg  28622  tgbtwnconn1lem3  28642  legso  28667  tglineeltr  28699  tglineintmo  28710  tglineneq  28712  colline  28717  mirne  28735  miriso  28738  mirhl  28747  mirbtwnhl  28748  symquadlem  28757  krippenlem  28758  midexlem  28760  ragncol  28777  footexALT  28786  footexlem2  28788  colperp  28797  colperpexlem3  28800  mideulem2  28802  opphllem  28803  midex  28805  opptgdim2  28813  oppperpex  28821  hlpasch  28824  colopp  28837  lmieu  28852  trgcopy  28872  cgracol  28896  cgrg3col4  28921  axlowdimlem15  29025  axcontlem2  29034  axcontlem7  29039  1egrvtxdg0  29580  2pthnloop  29799  cyclnspth  29869  eupth2lem1  30288  eupth2lem2  30289  eupth2lem3lem6  30303  nrt2irr  30543  strlem6  32327  hstrlem6  32335  atssma  32449  chirredlem1  32461  snsssng  32584  ifnetrue  32617  ifnefals  32618  fmptunsnop  32773  xaddeq0  32826  rexmul2  32827  xlt2addrd  32832  xnn0nn0d  32845  hashpss  32882  elq2  32885  divnumden2  32889  sgnmul  32908  sgn0bi  32913  2exple2exp  32918  pmtridf1o  33155  pmtridfv1  33156  pmtridfv2  33157  elrgspnlem2  33304  elrgspnlem3  33305  domnprodeq0  33337  fracfld  33369  pidlnz  33436  lindssn  33438  drngidl  33493  drngidlhash  33494  0ringprmidl  33509  qsidomlem1  33512  ssdifidlprm  33518  mxidlmaxv  33528  mxidlprm  33530  mxidlirredi  33531  mxidlirred  33532  krull  33539  rsprprmprmidlb  33583  rprmasso2  33586  pidufd  33603  1arithufdlem3  33606  dfufd2  33610  zringidom  33611  0ringmon1p  33617  ig1pnunit  33661  mplmulmvr  33683  psrmonmul  33694  esplyfval2  33709  esplymhp  33712  esplyfval3  33716  vietadeg1  33722  lindsunlem  33768  fldextrspundgdvdslem  33824  fldext2rspun  33826  ply1annnr  33847  fldext2chn  33872  constrextdg2lem  33892  constrext2chnlem  33894  constrcon  33918  2sqr3minply  33924  cos9thpiminply  33932  1smat1  33948  submatminr1  33954  madjusmdetlem2  33972  zarcls1  34013  zarclsint  34016  zarclssn  34017  xrge0iifcnv  34077  xrge0iifcv  34078  xrge0iif1  34082  qqhval2lem  34125  qqhf  34130  qqhre  34164  esumrnmpt2  34212  esumcvgre  34235  inelpisys  34298  carsgclctunlem2  34463  ballotlemirc  34676  signswlid  34703  repr0  34755  reprlt  34763  reprgt  34765  reprinfz1  34766  tgoldbachgtda  34805  tgoldbachgt  34807  bnj1523  35213  acycgr2v  35332  fmlaomn0  35572  fmlasucdisj  35581  fz0n  35913  dfrdg2  35975  dfrdg4  36133  broutsideof2  36304  outsidele  36314  rankeq1o  36353  ivthALT  36517  limsucncmpi  36627  mh-inf3sn  36724  qdiff  37641  topdifinffinlem  37663  icorempo  37667  finxpreclem2  37706  finxp1o  37708  finxpreclem6  37712  poimirlem9  37950  poimirlem11  37952  poimirlem12  37953  poimirlem25  37966  fdc  38066  heibor1lem  38130  heiborlem4  38135  heiborlem6  38137  disjressuc2  38732  2atm  39973  lhpocnle  40462  lhp2at0nle  40481  trlval3  40633  cdleme18c  40739  cdlemg17b  41108  cdlemg17i  41115  dia2dimlem2  41511  dia2dimlem3  41512  dihord6apre  41702  dihatlat  41780  dochshpsat  41900  lcfrlem9  41996  mapdhval2  42172  hdmap1val2  42246  hdmap14lem4a  42317  hdmap14lem6  42319  dvrelogpow2b  42507  aks4d1p1p4  42510  aks4d1p6  42520  fldhmf1  42529  primrootspoweq0  42545  aks6d1c2p2  42558  hashscontpow  42561  aks6d1c5  42578  sticksstones1  42585  sticksstones10  42594  sticksstones12a  42596  sticksstones12  42597  sticksstones22  42607  aks6d1c6lem4  42612  aks6d1c7lem1  42619  aks6d1c7  42623  aks5lem8  42640  negn0nposznnd  42714  mhpind  43027  prjspner1  43059  dffltz  43067  3cubeslem2  43117  jm2.26lem3  43429  kelac1  43491  cantnfresb  43752  tfsconcat0b  43774  nlimsuc  43868  clsk1indlem0  44468  scotteld  44673  sineq0ALT  45363  refsum2cnlem1  45468  disjxp1  45500  disjf1  45613  disjrnmpt2  45618  disjinfi  45622  oddfl  45711  xrlttri5d  45717  supxrge  45768  nepnfltpnf  45772  nemnftgtmnft  45774  xrlexaddrp  45782  xrred  45794  supminfxr2  45897  icoiccdif  45954  qinioo  45965  ioonct  45967  fmul01lt1lem1  46014  climrec  46033  limcperiod  46058  reclimc  46081  limsupub  46132  liminflbuz2  46243  cncfiooicclem1  46321  cncfioobdlem  46324  fperdvper  46347  dvdivbd  46351  ditgeqiooicc  46388  itgsincmulx  46402  itgioocnicc  46405  iblcncfioo  46406  stoweidlem35  46463  stoweidlem39  46467  stirlinglem5  46506  stirlinglem8  46509  dirkerper  46524  dirkercncflem2  46532  dirkercncflem4  46534  fourierdlem31  46566  fourierdlem34  46569  fourierdlem41  46576  fourierdlem42  46577  fourierdlem44  46579  fourierdlem48  46582  fourierdlem49  46583  fourierdlem53  46587  fourierdlem56  46590  fourierdlem58  46592  fourierdlem60  46594  fourierdlem61  46595  fourierdlem62  46596  fourierdlem65  46599  fourierdlem66  46600  fourierdlem73  46607  fourierdlem76  46610  fourierdlem79  46613  fourierdlem81  46615  fourierdlem82  46616  fourierdlem93  46627  fourierdlem103  46637  fourierdlem104  46638  sqwvfoura  46656  fourierswlem  46658  elaa2lem  46661  elaa2  46662  etransclem4  46666  etransclem24  46686  etransclem31  46693  etransclem32  46694  etransclem35  46697  sge0repnf  46814  sge0fodjrnlem  46844  sge0iunmpt  46846  sge0rpcpnf  46849  nnfoctbdjlem  46883  meadjun  46890  voliunsge0lem  46900  hoicvr  46976  ovnn0val  46979  ovnsubaddlem1  46998  hoidmvn0val  47012  hsphoidmvle  47014  hoidmv1lelem1  47019  hoidmv1lelem2  47020  hoidmv1lelem3  47021  ovnhoilem1  47029  ovnsubadd2lem  47073  ovnovollem3  47086  cjnpoly  47337  lighneallem3  48070  divgcdoddALTV  48158  isubgr0uhgr  48349  usgrexmpl2trifr  48513  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  dignn0flhalflem1  49091  itcoval2  49140  itcoval3  49141  itcovalsuc  49143  ackvalsuc1mpt  49154  line2xlem  49229