Theorem neneqd 2941

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1548   ≠ wne 2936

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 209  df-ne 2937

This theorem is referenced by:  neneq  2942  necon2bi  2966  necon2i  2970  necon4i  2971  pm2.21ddne  3020  mteqand  3027  nelrdva  3648  eldifsnneq  4727  disjprg  5071  0inp0  5290  nelrnmpt  5916  rnmptn0  6199  resf1extb  7878  frxp2  8088  frxp3  8095  onnseq  8278  finnzfsuppd  9280  sniffsupp  9307  dfac2b  10048  ackbij1lem15  10150  ttukeylem7  10432  fpwwe2lem12  10560  canthnumlem  10566  canthp1lem2  10571  recgt0  11996  nnneneg  12207  elnnz  12529  xrnemnf  13063  xrnepnf  13064  fzprval  13534  fzodisjsn  13647  fzone1  13734  expnnval  14021  znsqcld  14119  hashelne0d  14325  elprchashprn2  14353  relexpsucnnr  14982  relexp1g  14983  relexpuzrel  15009  sgnp  15047  fprodn0f  15951  ruclem12  16203  dvdsle  16274  nndvdslegcd  16469  gcdnncl  16471  divgcdnn  16479  nn0rppwr  16525  sqgcd  16526  eucalgf  16547  eucalginv  16548  lcmgcdlem  16570  lcmftp  16600  lcmfunsnlem2lem1  16602  lcmfunsnlem2lem2  16603  qredeu  16622  rpdvds  16624  cncongr2  16632  divnumden  16713  divdenle  16714  phisum  16756  oddprm  16776  pythagtriplem4  16785  pythagtriplem8  16789  pythagtriplem9  16790  4sqlem10  16913  ram0  16988  cat1lem  18058  isipodrs  18498  chnub  18583  chnpof1  18591  gsumval2  18649  smndex1n0mnd  18878  smndex2dnrinv  18881  mulgnn  19046  sylow1lem1  19568  gsumval3eu  19874  ablsimpgfindlem1  20079  ablsimpgfindlem2  20080  ablsimpgfind  20082  fincygsubgodd  20084  submomnd  20102  rrgnz  20680  fidomndrng  20749  abvtrivd  20808  ornglmullt  20845  orngrmullt  20846  suborng  20852  00lss  20935  lvecvscan2  21109  prmirredlem  21451  ofldchr  21555  uvcff  21770  mvrcl  21970  mplmon  22015  mplmonmul  22016  psdmul  22158  coe1tmfv2  22265  cply1coe0  22291  cply1coe0bi  22292  1marepvsma1  22570  mdetrsca2  22591  mdetrlin2  22594  mdetunilem2  22600  mdetunilem5  22603  mdetunilem6  22604  mdetunilem9  22607  maducoeval2  22627  gsummatr01lem3  22644  gsummatr01lem4  22645  gsummatr01  22646  m2cpm  22728  m2cpminvid2lem  22741  fvmptnn04ifa  22837  fvmptnn04ifb  22838  fvmptnn04ifc  22839  chfacffsupp  22843  chfacfscmul0  22845  chfacfscmulgsum  22847  chfacfpmmul0  22849  chfacfpmmulgsum  22851  connclo  23402  dissnlocfin  23516  ptpjpre2  23567  txindis  23621  snfil  23851  alexsublem  24031  tsmsfbas  24115  stdbdxmet  24502  dscmet  24559  xrsxmet  24797  iccpnfcnv  24933  cphsubrglem  25166  minveclem3b  25417  minveclem4a  25419  ovolicc1  25505  dvexp2  25943  dvmptdiv  25963  lhop2  26004  deg1sublt  26097  ig1pval3  26165  dvply1  26272  plydiveu  26286  quotcan  26297  aaliou3lem9  26338  taylthlem2  26361  pserdvlem2  26415  abelthlem9  26427  logccne0  26564  logtayllem  26645  logtayl  26646  cxpef  26651  rtprmirr  26746  angrtmuld  26794  isosctrlem3  26806  chordthmlem  26818  leibpilem2  26927  leibpi  26928  rlimcnp2  26952  efrlim  26955  vma1  27151  muinv  27178  lgsval2lem  27292  lgsval4  27302  lgsdir  27317  lgseisenlem4  27363  lgsquadlem1  27365  lgsquad2  27371  m1lgs  27373  2sqlem8a  27410  2sqlem8  27411  2sqcoprm  27420  2sqmod  27421  padicabv  27615  ostth1  27618  ostth3  27623  nolesgn2ores  27658  nogesgn1ores  27660  nosep1o  27667  nosep2o  27668  nosepdmlem  27669  nosepssdm  27672  noresle  27683  nosupbnd1lem3  27696  nosupbnd1lem4  27697  nosupbnd1lem5  27698  nosupbnd1lem6  27699  nosupbnd2lem1  27701  noinfbnd1lem3  27711  noinfbnd1lem4  27712  noinfbnd1lem5  27713  noinfbnd1lem6  27714  noinfbnd2lem1  27716  0elold  27924  elnnzs  28415  expnnsval  28440  expsne0  28450  bdayfinbndlem1  28481  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  29602  2pthnloop  29821  cyclnspth  29891  eupth2lem1  30310  eupth2lem2  30311  eupth2lem3lem6  30325  nrt2irr  30565  strlem6  32349  hstrlem6  32357  atssma  32471  chirredlem1  32483  snsssng  32606  ifnetrue  32639  ifnefals  32640  fmptunsnop  32796  xaddeq0  32849  rexmul2  32850  xlt2addrd  32855  xnn0nn0d  32868  hashpss  32905  elq2  32908  divnumden2  32912  sgnmul  32931  sgn0bi  32936  2exple2exp  32941  pmtridf1o  33179  pmtridfv1  33180  pmtridfv2  33181  elrgspnlem2  33328  elrgspnlem3  33329  domnprodeq0  33361  fracfld  33396  pidlnz  33463  lindssn  33465  drngidl  33520  drngidlhash  33521  0ringprmidl  33536  qsidomlem1  33539  ssdifidlprm  33545  mxidlmaxv  33555  mxidlprm  33557  mxidlirredi  33558  mxidlirred  33559  krull  33566  drnglring  33587  dflring3  33592  dflring4  33593  rsprprmprmidlb  33618  rprmasso2  33621  pidufd  33638  1arithufdlem3  33641  dfufd2  33645  zringidom  33646  0ringmon1p  33652  ig1pnunit  33696  mplmulmvr  33735  psrmonmul  33746  esplyfval2  33761  esplymhp  33764  esplyfval3  33768  vietadeg1  33774  lindsunlem  33820  fldextrspundgdvdslem  33876  fldext2rspun  33878  ply1annnr  33899  fldext2chn  33924  constrextdg2lem  33944  constrext2chnlem  33946  constrcon  33970  2sqr3minply  33976  cos9thpiminply  33984  1smat1  34000  submatminr1  34006  madjusmdetlem2  34024  zarcls1  34065  zarclsint  34068  zarclssn  34069  xrge0iifcnv  34129  xrge0iifcv  34130  xrge0iif1  34134  qqhval2lem  34177  qqhf  34182  qqhre  34216  esumrnmpt2  34264  esumcvgre  34287  inelpisys  34350  carsgclctunlem2  34515  ballotlemirc  34728  signswlid  34755  repr0  34807  reprlt  34815  reprgt  34817  reprinfz1  34818  tgoldbachgtda  34857  tgoldbachgt  34859  bnj1523  35268  acycgr2v  35393  fmlaomn0  35633  fmlasucdisj  35642  fz0n  35974  dfrdg2  36036  dfrdg4  36194  broutsideof2  36365  outsidele  36375  rankeq1o  36414  ivthALT  36578  limsucncmpi  36688  mh-inf3sn  36785  qdiff  37702  topdifinffinlem  37724  icorempo  37728  finxpreclem2  37767  finxp1o  37769  finxpreclem6  37773  poimirlem9  38011  poimirlem11  38013  poimirlem12  38014  poimirlem25  38027  fdc  38127  heibor1lem  38191  heiborlem4  38196  heiborlem6  38198  disjressuc2  38793  2atm  40034  lhpocnle  40523  lhp2at0nle  40542  trlval3  40694  cdleme18c  40800  cdlemg17b  41169  cdlemg17i  41176  dia2dimlem2  41572  dia2dimlem3  41573  dihord6apre  41763  dihatlat  41841  dochshpsat  41961  lcfrlem9  42057  mapdhval2  42233  hdmap1val2  42307  hdmap14lem4a  42378  hdmap14lem6  42380  dvrelogpow2b  42568  aks4d1p1p4  42571  aks4d1p6  42581  fldhmf1  42590  primrootspoweq0  42606  aks6d1c2p2  42619  hashscontpow  42622  aks6d1c5  42639  sticksstones1  42646  sticksstones10  42655  sticksstones12a  42657  sticksstones12  42658  sticksstones22  42668  aks6d1c6lem4  42673  aks6d1c7lem1  42680  aks6d1c7  42684  aks5lem8  42701  negn0nposznnd  42774  mhpind  43059  prjspner1  43091  dffltz  43099  3cubeslem2  43149  jm2.26lem3  43461  kelac1  43523  cantnfresb  43784  tfsconcat0b  43806  nlimsuc  43900  clsk1indlem0  44500  scotteld  44705  sineq0ALT  45395  refsum2cnlem1  45500  disjxp1  45532  disjf1  45644  disjrnmpt2  45649  disjinfi  45653  oddfl  45740  xrlttri5d  45746  supxrge  45797  nepnfltpnf  45801  nemnftgtmnft  45803  xrlexaddrp  45811  xrred  45823  supminfxr2  45926  icoiccdif  45983  qinioo  45994  ioonct  45996  fmul01lt1lem1  46043  climrec  46062  limcperiod  46087  reclimc  46110  limsupub  46161  liminflbuz2  46272  cncfiooicclem1  46350  cncfioobdlem  46353  fperdvper  46376  dvdivbd  46380  ditgeqiooicc  46417  itgsincmulx  46431  itgioocnicc  46434  iblcncfioo  46435  stoweidlem35  46492  stoweidlem39  46496  stirlinglem5  46535  stirlinglem8  46538  dirkerper  46553  dirkercncflem2  46561  dirkercncflem4  46563  fourierdlem31  46595  fourierdlem34  46598  fourierdlem41  46605  fourierdlem42  46606  fourierdlem44  46608  fourierdlem48  46611  fourierdlem49  46612  fourierdlem53  46616  fourierdlem56  46619  fourierdlem58  46621  fourierdlem60  46623  fourierdlem61  46624  fourierdlem62  46625  fourierdlem65  46628  fourierdlem66  46629  fourierdlem73  46636  fourierdlem76  46639  fourierdlem79  46642  fourierdlem81  46644  fourierdlem82  46645  fourierdlem93  46656  fourierdlem103  46666  fourierdlem104  46667  sqwvfoura  46685  fourierswlem  46687  elaa2lem  46690  elaa2  46691  etransclem4  46695  etransclem24  46715  etransclem31  46722  etransclem32  46723  etransclem35  46726  sge0repnf  46843  sge0fodjrnlem  46873  sge0iunmpt  46875  sge0rpcpnf  46878  nnfoctbdjlem  46912  meadjun  46919  voliunsge0lem  46929  hoicvr  47005  ovnn0val  47008  ovnsubaddlem1  47027  hoidmvn0val  47041  hsphoidmvle  47043  hoidmv1lelem1  47048  hoidmv1lelem2  47049  hoidmv1lelem3  47050  ovnhoilem1  47058  ovnsubadd2lem  47102  ovnovollem3  47115  cjnpoly  47366  lighneallem3  48099  divgcdoddALTV  48187  isubgr0uhgr  48378  usgrexmpl2trifr  48542  gpg5nbgrvtx03star  48585  gpg5nbgr3star  48586  dignn0flhalflem1  49120  itcoval2  49169  itcoval3  49170  itcovalsuc  49172  ackvalsuc1mpt  49183  line2xlem  49258