Theorem neneqd 2938

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

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

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 2934

This theorem is referenced by:  neneq  2939  necon2bi  2963  necon2i  2967  necon4i  2968  pm2.21ddne  3017  mteqand  3024  nelrdva  3665  eldifsnneq  4749  disjprg  5096  0inp0  5308  nelrnmpt  5926  rnmptn0  6212  resf1extb  7888  frxp2  8098  frxp3  8105  onnseq  8288  finnzfsuppd  9290  sniffsupp  9317  dfac2b  10055  ackbij1lem15  10157  ttukeylem7  10439  fpwwe2lem12  10567  canthnumlem  10573  canthp1lem2  10578  recgt0  12001  nnneneg  12194  elnnz  12512  xrnemnf  13045  xrnepnf  13046  fzprval  13515  fzodisjsn  13627  fzone1  13714  expnnval  14001  znsqcld  14099  hashelne0d  14305  elprchashprn2  14333  relexpsucnnr  14962  relexp1g  14963  relexpuzrel  14989  sgnp  15027  fprodn0f  15928  ruclem12  16180  dvdsle  16251  nndvdslegcd  16446  gcdnncl  16448  divgcdnn  16456  nn0rppwr  16502  sqgcd  16503  eucalgf  16524  eucalginv  16525  lcmgcdlem  16547  lcmftp  16577  lcmfunsnlem2lem1  16579  lcmfunsnlem2lem2  16580  qredeu  16599  rpdvds  16601  cncongr2  16609  divnumden  16689  divdenle  16690  phisum  16732  oddprm  16752  pythagtriplem4  16761  pythagtriplem8  16765  pythagtriplem9  16766  4sqlem10  16889  ram0  16964  cat1lem  18034  isipodrs  18474  chnub  18559  chnpof1  18567  gsumval2  18625  smndex1n0mnd  18854  smndex2dnrinv  18857  mulgnn  19022  sylow1lem1  19544  gsumval3eu  19850  ablsimpgfindlem1  20055  ablsimpgfindlem2  20056  ablsimpgfind  20058  fincygsubgodd  20060  submomnd  20078  rrgnz  20654  fidomndrng  20723  abvtrivd  20782  ornglmullt  20819  orngrmullt  20820  suborng  20826  00lss  20909  lvecvscan2  21084  prmirredlem  21444  ofldchr  21548  uvcff  21763  mvrcl  21964  mplmon  22007  mplmonmul  22008  psdmul  22126  coe1tmfv2  22234  cply1coe0  22262  cply1coe0bi  22263  1marepvsma1  22544  mdetrsca2  22565  mdetrlin2  22568  mdetunilem2  22574  mdetunilem5  22577  mdetunilem6  22578  mdetunilem9  22581  maducoeval2  22601  gsummatr01lem3  22618  gsummatr01lem4  22619  gsummatr01  22620  m2cpm  22702  m2cpminvid2lem  22715  fvmptnn04ifa  22811  fvmptnn04ifb  22812  fvmptnn04ifc  22813  chfacffsupp  22817  chfacfscmul0  22819  chfacfscmulgsum  22821  chfacfpmmul0  22823  chfacfpmmulgsum  22825  connclo  23376  dissnlocfin  23490  ptpjpre2  23541  txindis  23595  snfil  23825  alexsublem  24005  tsmsfbas  24089  stdbdxmet  24476  dscmet  24533  xrsxmet  24771  iccpnfcnv  24915  cphsubrglem  25150  minveclem3b  25401  minveclem4a  25403  ovolicc1  25490  dvexp2  25931  dvmptdiv  25951  lhop2  25993  deg1sublt  26088  ig1pval3  26156  dvply1  26264  plydiveu  26279  quotcan  26290  aaliou3lem9  26331  taylthlem2  26355  taylthlem2OLD  26356  pserdvlem2  26411  abelthlem9  26423  logccne0  26560  logtayllem  26641  logtayl  26642  cxpef  26647  rtprmirr  26743  angrtmuld  26791  isosctrlem3  26803  chordthmlem  26815  leibpilem2  26924  leibpi  26925  rlimcnp2  26949  efrlim  26952  efrlimOLD  26953  vma1  27149  muinv  27176  lgsval2lem  27291  lgsval4  27301  lgsdir  27316  lgseisenlem4  27362  lgsquadlem1  27364  lgsquad2  27370  m1lgs  27372  2sqlem8a  27409  2sqlem8  27410  2sqcoprm  27419  2sqmod  27420  padicabv  27614  ostth1  27617  ostth3  27622  nolesgn2ores  27657  nogesgn1ores  27659  nosep1o  27666  nosep2o  27667  nosepdmlem  27668  nosepssdm  27671  noresle  27682  nosupbnd1lem3  27695  nosupbnd1lem4  27696  nosupbnd1lem5  27697  nosupbnd1lem6  27698  nosupbnd2lem1  27700  noinfbnd1lem3  27710  noinfbnd1lem4  27711  noinfbnd1lem5  27712  noinfbnd1lem6  27713  noinfbnd2lem1  27715  0elold  27923  elnnzs  28414  expnnsval  28439  expsne0  28449  bdayfinbndlem1  28480  tgbtwnne  28580  tgbtwndiff  28596  tgcolg  28644  tgbtwnconn1lem3  28664  legso  28689  tglineeltr  28721  tglineintmo  28732  tglineneq  28734  colline  28739  mirne  28757  miriso  28760  mirhl  28769  mirbtwnhl  28770  symquadlem  28779  krippenlem  28780  midexlem  28782  ragncol  28799  footexALT  28808  footexlem2  28810  colperp  28819  colperpexlem3  28822  mideulem2  28824  opphllem  28825  midex  28827  opptgdim2  28835  oppperpex  28843  hlpasch  28846  colopp  28859  lmieu  28874  trgcopy  28894  cgracol  28918  cgrg3col4  28943  axlowdimlem15  29047  axcontlem2  29056  axcontlem7  29061  1egrvtxdg0  29603  2pthnloop  29822  cyclnspth  29892  eupth2lem1  30311  eupth2lem2  30312  eupth2lem3lem6  30326  nrt2irr  30566  strlem6  32350  hstrlem6  32358  atssma  32472  chirredlem1  32484  snsssng  32607  ifnetrue  32640  ifnefals  32641  fmptunsnop  32796  xaddeq0  32850  rexmul2  32851  xlt2addrd  32856  xnn0nn0d  32869  hashpss  32906  elq2  32909  divnumden2  32913  sgnmul  32933  sgn0bi  32938  2exple2exp  32943  pmtridf1o  33194  pmtridfv1  33195  pmtridfv2  33196  elrgspnlem2  33343  elrgspnlem3  33344  domnprodeq0  33376  fracfld  33408  pidlnz  33475  lindssn  33477  drngidl  33532  drngidlhash  33533  0ringprmidl  33548  qsidomlem1  33551  ssdifidlprm  33557  mxidlmaxv  33567  mxidlprm  33569  mxidlirredi  33570  mxidlirred  33571  krull  33578  rsprprmprmidlb  33622  rprmasso2  33625  pidufd  33642  1arithufdlem3  33645  dfufd2  33649  zringidom  33650  0ringmon1p  33656  ig1pnunit  33700  mplmulmvr  33722  psrmonmul  33733  esplyfval2  33748  esplymhp  33751  esplyfval3  33755  vietadeg1  33761  lindsunlem  33808  fldextrspundgdvdslem  33864  fldext2rspun  33866  ply1annnr  33887  fldext2chn  33912  constrextdg2lem  33932  constrext2chnlem  33934  constrcon  33958  2sqr3minply  33964  cos9thpiminply  33972  1smat1  33988  submatminr1  33994  madjusmdetlem2  34012  zarcls1  34053  zarclsint  34056  zarclssn  34057  xrge0iifcnv  34117  xrge0iifcv  34118  xrge0iif1  34122  qqhval2lem  34165  qqhf  34170  qqhre  34204  esumrnmpt2  34252  esumcvgre  34275  inelpisys  34338  carsgclctunlem2  34503  ballotlemirc  34716  signswlid  34743  repr0  34795  reprlt  34803  reprgt  34805  reprinfz1  34806  tgoldbachgtda  34845  tgoldbachgt  34847  bnj1523  35253  acycgr2v  35372  fmlaomn0  35612  fmlasucdisj  35621  fz0n  35953  dfrdg2  36015  dfrdg4  36173  broutsideof2  36344  outsidele  36354  rankeq1o  36393  ivthALT  36557  limsucncmpi  36667  topdifinffinlem  37629  icorempo  37633  finxpreclem2  37672  finxp1o  37674  finxpreclem6  37678  poimirlem9  37909  poimirlem11  37911  poimirlem12  37912  poimirlem25  37925  fdc  38025  heibor1lem  38089  heiborlem4  38094  heiborlem6  38096  disjressuc2  38691  2atm  39932  lhpocnle  40421  lhp2at0nle  40440  trlval3  40592  cdleme18c  40698  cdlemg17b  41067  cdlemg17i  41074  dia2dimlem2  41470  dia2dimlem3  41471  dihord6apre  41661  dihatlat  41739  dochshpsat  41859  lcfrlem9  41955  mapdhval2  42131  hdmap1val2  42205  hdmap14lem4a  42276  hdmap14lem6  42278  dvrelogpow2b  42467  aks4d1p1p4  42470  aks4d1p6  42480  fldhmf1  42489  primrootspoweq0  42505  aks6d1c2p2  42518  hashscontpow  42521  aks6d1c5  42538  sticksstones1  42545  sticksstones10  42554  sticksstones12a  42556  sticksstones12  42557  sticksstones22  42567  aks6d1c6lem4  42572  aks6d1c7lem1  42579  aks6d1c7  42583  aks5lem8  42600  negn0nposznnd  42681  mhpind  42981  prjspner1  43013  dffltz  43021  3cubeslem2  43071  jm2.26lem3  43387  kelac1  43449  cantnfresb  43710  tfsconcat0b  43732  nlimsuc  43826  clsk1indlem0  44426  scotteld  44631  sineq0ALT  45321  refsum2cnlem1  45426  disjxp1  45458  disjf1  45571  disjrnmpt2  45576  disjinfi  45580  oddfl  45669  xrlttri5d  45675  supxrge  45726  nepnfltpnf  45730  nemnftgtmnft  45732  xrlexaddrp  45740  xrred  45752  supminfxr2  45856  icoiccdif  45913  qinioo  45924  ioonct  45926  fmul01lt1lem1  45973  climrec  45992  limcperiod  46017  reclimc  46040  limsupub  46091  liminflbuz2  46202  cncfiooicclem1  46280  cncfioobdlem  46283  fperdvper  46306  dvdivbd  46310  ditgeqiooicc  46347  itgsincmulx  46361  itgioocnicc  46364  iblcncfioo  46365  stoweidlem35  46422  stoweidlem39  46426  stirlinglem5  46465  stirlinglem8  46468  dirkerper  46483  dirkercncflem2  46491  dirkercncflem4  46493  fourierdlem31  46525  fourierdlem34  46528  fourierdlem41  46535  fourierdlem42  46536  fourierdlem44  46538  fourierdlem48  46541  fourierdlem49  46542  fourierdlem53  46546  fourierdlem56  46549  fourierdlem58  46551  fourierdlem60  46553  fourierdlem61  46554  fourierdlem62  46555  fourierdlem65  46558  fourierdlem66  46559  fourierdlem73  46566  fourierdlem76  46569  fourierdlem79  46572  fourierdlem81  46574  fourierdlem82  46575  fourierdlem93  46586  fourierdlem103  46596  fourierdlem104  46597  sqwvfoura  46615  fourierswlem  46617  elaa2lem  46620  elaa2  46621  etransclem4  46625  etransclem24  46645  etransclem31  46652  etransclem32  46653  etransclem35  46656  sge0repnf  46773  sge0fodjrnlem  46803  sge0iunmpt  46805  sge0rpcpnf  46808  nnfoctbdjlem  46842  meadjun  46849  voliunsge0lem  46859  hoicvr  46935  ovnn0val  46938  ovnsubaddlem1  46957  hoidmvn0val  46971  hsphoidmvle  46973  hoidmv1lelem1  46978  hoidmv1lelem2  46979  hoidmv1lelem3  46980  ovnhoilem1  46988  ovnsubadd2lem  47032  ovnovollem3  47045  cjnpoly  47278  lighneallem3  47996  divgcdoddALTV  48071  isubgr0uhgr  48262  usgrexmpl2trifr  48426  gpg5nbgrvtx03star  48469  gpg5nbgr3star  48470  dignn0flhalflem1  49004  itcoval2  49053  itcoval3  49054  itcovalsuc  49056  ackvalsuc1mpt  49067  line2xlem  49142