Theorem neneqd 2960

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2955

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2956

This theorem is used by:  neneq  2961  necon2bi  2985  necon2i  2989  necon4i  2990  pm2.21ddne  3039  mteqand  3046  nelrdva  3663  nrmod  3839  eldifsnneq  4754  disjprg  5099  0inp0  5320  nelrnmpt  5946  rnmptn0  6235  resf1extb  7930  frxp2  8140  frxp3  8147  onnseq  8331  finnzfsuppd  9343  sniffsupp  9370  scotteld  9904  dfac2b  10166  ackbij1lem15  10268  ttukeylem7  10550  fpwwe2lem12  10684  canthnumlem  10690  canthp1lem2  10695  recgt0  12118  nnneneg  12328  elnnz  12658  xrnemnf  13201  xrnepnf  13202  fzprval  13673  fzodisjsn  13786  fzone1  13873  expnnval  14161  znsqcld  14259  hashelne0d  14465  elprchashprn2  14493  hashpss  14507  relexpsucnnr  15131  relexp1g  15132  relexpuzrel  15158  sgnp  15196  sgn0bi  15209  sgnmul  15213  fprodn0f  16111  ruclem12  16362  dvdsle  16433  nndvdslegcd  16628  gcdnncl  16630  divgcdnn  16638  nn0rppwr  16684  sqgcd  16685  eucalgf  16706  eucalginv  16707  lcmgcdlem  16729  lcmftp  16759  lcmfunsnlem2lem1  16761  lcmfunsnlem2lem2  16762  qredeu  16781  rpdvds  16783  cncongr2  16791  divnumden  16872  divdenle  16873  phisum  16915  oddprm  16935  pythagtriplem4  16944  pythagtriplem8  16948  pythagtriplem9  16949  4sqlem10  17072  ram0  17147  cat1lem  18218  isipodrs  18658  chnub  18743  chnpof1  18751  gsumval2  18822  smndex1n0mnd  19058  smndex2dnrinv  19061  mulgnn  19232  sylow1lem1  19759  gsumval3eu  20065  ablsimpgfindlem1  20270  ablsimpgfindlem2  20271  ablsimpgfind  20273  fincygsubgodd  20275  submomnd  20293  rrgnz  20903  fidomndrng  20978  abvtrivd  21036  ornglmullt  21073  orngrmullt  21074  suborng  21080  00lss  21163  lvecvscan2  21337  pidlnz  21475  drngidl  21486  0ringprmidl  21580  qsidomlem1  21583  ssdifidlprm  21589  prmirredlem  21725  ofldchr  21829  uvcff  22044  mvrcl  22246  mplmon  22291  mplmonmul  22292  psdmul  22434  coe1tmfv2  22541  cply1coe0  22566  cply1coe0bi  22567  1marepvsma1  22845  mdetrsca2  22866  mdetrlin2  22869  mdetunilem2  22875  mdetunilem5  22878  mdetunilem6  22879  mdetunilem9  22882  maducoeval2  22902  gsummatr01lem3  22919  gsummatr01lem4  22920  gsummatr01  22921  m2cpm  23006  m2cpminvid2lem  23019  fvmptnn04ifa  23115  fvmptnn04ifb  23116  fvmptnn04ifc  23117  chfacffsupp  23121  chfacfscmul0  23123  chfacfscmulgsum  23125  chfacfpmmul0  23127  chfacfpmmulgsum  23129  connclo  23680  dissnlocfin  23795  ptpjpre2  23846  txindis  23900  snfil  24130  alexsublem  24310  tsmsfbas  24394  stdbdxmet  24781  dscmet  24838  xrsxmet  25076  iccpnfcnv  25212  cphsubrglem  25445  minveclem3b  25696  minveclem4a  25698  ovolicc1  25784  dvexp2  26221  dvmptdiv  26241  lhop2  26282  deg1sublt  26375  ig1pval3  26443  dvply1  26554  plydiveu  26568  rnplynfin  26579  quotcan  26581  aaliou3lem9  26626  taylthlem2  26650  pserdvlem2  26704  abelthlem9  26716  logccne0  26855  logtayllem  26936  logtayl  26937  cxpef  26942  rtprmirr  27037  angrtmuld  27085  isosctrlem3  27097  chordthmlem  27109  leibpilem2  27218  leibpi  27219  rlimcnp2  27243  efrlim  27246  vma1  27442  muinv  27469  lgsval2lem  27583  lgsval4  27593  lgsdir  27608  lgseisenlem4  27654  lgsquadlem1  27656  lgsquad2  27662  m1lgs  27664  2sqlem8a  27701  2sqlem8  27702  2sqcoprm  27711  2sqmod  27712  padicabv  27906  ostth1  27909  ostth3  27914  nolesgn2ores  27948  nogesgn1ores  27950  nosep1o  27957  nosep2o  27958  nosepdmlem  27959  nosepssdm  27962  noresle  27973  nosupbnd1lem3  27986  nosupbnd1lem4  27987  nosupbnd1lem5  27988  nosupbnd1lem6  27989  nosupbnd2lem1  27991  noinfbnd1lem3  28001  noinfbnd1lem4  28002  noinfbnd1lem5  28003  noinfbnd1lem6  28004  noinfbnd2lem1  28006  0elold  28215  elnnzs  28706  expnnsval  28731  expsne0  28741  bdayfinbndlem1  28772  tgbtwnne  28872  tgbtwndiff  28888  tgcolg  28936  tgbtwnconn1lem3  28956  legso  28981  tglineeltr  29018  tglineintmo  29029  tglineneq  29032  colline  29037  tglnpt4  29042  mirne  29058  miriso  29061  mirhl  29070  mirbtwnhl  29071  symquadlem  29080  krippenlem  29081  midexlem  29083  symquadprlnglem  29084  ragncol  29103  footexALT  29112  footexlem2  29114  colperp  29124  colperpexlem3  29127  mideulem2  29129  opphllem  29130  midex  29132  opptgdim2  29140  oppperpex  29148  hlpasch  29153  colopp  29166  lnincplng  29181  plngrotlem1  29184  plngrotlem2  29185  lnssplnglem  29188  lnssplng  29189  lmieu  29208  trgcopy  29230  cgracol  29255  tgaaddcpbllem1  29268  tgaaddcpbl  29271  tgaaddcpbl2  29272  cgrg3col4  29291  angmgmaddeu1  29298  angmgmaddov2lem  29306  angmgmaddcpbl  29309  prlngin0  29341  prlngpln  29342  prlnghpg  29343  dfprlng2  29344  prlngex  29348  prlngmolem1  29349  prlngmolem2  29350  prlngmo2  29353  prlngpln4  29355  prlnginn0  29357  prlngmid2  29358  prlngsymquadlem  29360  tgaltai  29364  axlowdimlem15  29453  axcontlem2  29462  axcontlem7  29467  1egrvtxdg0  30011  2pthnloop  30236  cyclnspth  30308  eupth2lem1  30738  eupth2lem2  30739  eupth2lem3lem6  30753  nrt2irr  30993  strlem6  32777  hstrlem6  32785  atssma  32899  chirredlem1  32911  snsssng  33029  ifnetrue  33062  ifnefals  33063  fmptunsnop  33212  xaddeq0  33264  rexmul2  33265  xlt2addrd  33270  xnn0nn0d  33283  elq2  33322  divnumden2  33326  2exple2exp  33344  pmtridf1o  33574  pmtridfv1  33575  pmtridfv2  33576  elrgspnlem2  33723  elrgspnlem3  33724  domnprodeq0  33759  fracfld  33789  lindssn  33852  drngidlhash  33902  mxidlmaxv  33912  mxidlprm  33914  mxidlirredi  33915  mxidlirred  33916  krull  33922  drnglring  33943  dflring3  33948  dflring4  33949  rsprprmprmidlb  33974  rprmasso2  33977  pidufd  33994  1arithufdlem3  33997  dfufd2  34001  zringidom  34002  0ringmon1p  34008  ig1pnunit  34052  mplmulmvr  34090  psrmonmul  34101  esplyfval2  34116  esplymhp  34119  esplyfval3  34123  vietadeg1  34129  lindsunlem  34175  fldextrspundgdvdslem  34231  fldext2rspun  34233  ply1annnr  34254  fldext2chn  34279  constrextdg2lem  34299  constrext2chnlem  34301  constrcon  34325  2sqr3minply  34331  cos9thpiminply  34339  1smat1  34355  submatminr1  34361  madjusmdetlem2  34379  zarcls1  34420  zarclsint  34423  zarclssn  34424  xrge0iifcnv  34484  xrge0iifcv  34485  xrge0iif1  34489  qqhval2lem  34532  qqhf  34537  qqhre  34571  esumrnmpt2  34619  esumcvgre  34642  inelpisys  34706  carsgclctunlem2  34871  ballotlemirc  35084  signswlid  35108  repr0  35160  reprlt  35168  reprgt  35170  reprinfz1  35171  tgoldbachgtda  35210  tgoldbachgt  35212  bnj1523  35621  kard0b  35746  acycgr2v  35830  fmlaomn0  36070  fmlasucdisj  36079  fz0n  36411  dfrdg2  36473  dfrdg4  36631  broutsideof2  36803  outsidele  36813  rankeq1o  36848  ivthALT  37039  limsucncmpi  37149  mh-inf3sn  37246  qdiff  38162  topdifinffinlem  38184  icorempo  38188  finxpreclem2  38227  finxp1o  38229  finxpreclem6  38233  poimirlem9  38461  poimirlem11  38463  poimirlem12  38464  poimirlem25  38477  fdc  38593  heibor1lem  38657  heiborlem4  38662  heiborlem6  38664  disjressuc2  39257  2atm  40498  lhpocnle  40987  lhp2at0nle  41006  trlval3  41158  cdleme18c  41264  cdlemg17b  41633  cdlemg17i  41640  dia2dimlem2  42036  dia2dimlem3  42037  dihord6apre  42227  dihatlat  42305  dochshpsat  42425  lcfrlem9  42521  mapdhval2  42697  hdmap1val2  42771  hdmap14lem4a  42842  hdmap14lem6  42844  dvrelogpow2b  43032  aks4d1p1p4  43035  aks4d1p6  43045  fldhmf1  43054  primrootspoweq0  43070  aks6d1c2p2  43083  hashscontpow  43086  aks6d1c5  43103  sticksstones1  43110  sticksstones10  43119  sticksstones12a  43121  sticksstones12  43122  sticksstones22  43132  aks6d1c6lem4  43137  aks6d1c7lem1  43144  aks6d1c7  43148  aks5lem8  43165  quadfac  43169  negn0nposznnd  43255  mhpind  43538  prjspner1  43570  dffltz  43578  3cubeslem2  43628  jm2.26lem3  43940  kelac1  44002  cantnfresb  44263  tfsconcat0b  44285  nlimsuc  44379  clsk1indlem0  44979  sineq0ALT  45857  refsum2cnlem1  45969  disjxp1  46001  disjf1  46113  disjrnmpt2  46118  disjinfi  46122  oddfl  46209  xrlttri5d  46215  supxrge  46266  nepnfltpnf  46270  nemnftgtmnft  46272  xrlexaddrp  46280  xrred  46292  supminfxr2  46395  icoiccdif  46452  qinioo  46463  ioonct  46465  fmul01lt1lem1  46512  climrec  46531  limcperiod  46556  reclimc  46579  limsupub  46630  liminflbuz2  46741  cncfiooicclem1  46819  cncfioobdlem  46822  fperdvper  46845  dvdivbd  46849  ditgeqiooicc  46886  itgsincmulx  46900  itgioocnicc  46903  iblcncfioo  46904  stoweidlem35  46961  stoweidlem39  46965  stirlinglem5  47004  stirlinglem8  47007  dirkerper  47022  dirkercncflem2  47030  dirkercncflem4  47032  fourierdlem31  47064  fourierdlem34  47067  fourierdlem41  47074  fourierdlem42  47075  fourierdlem44  47077  fourierdlem48  47080  fourierdlem49  47081  fourierdlem53  47085  fourierdlem56  47088  fourierdlem58  47090  fourierdlem60  47092  fourierdlem61  47093  fourierdlem62  47094  fourierdlem65  47097  fourierdlem66  47098  fourierdlem73  47105  fourierdlem76  47108  fourierdlem79  47111  fourierdlem81  47113  fourierdlem82  47114  fourierdlem93  47125  fourierdlem103  47135  fourierdlem104  47136  sqwvfoura  47154  fourierswlem  47156  elaa2lem  47159  elaa2  47160  etransclem4  47164  etransclem24  47184  etransclem31  47191  etransclem32  47192  etransclem35  47195  sge0repnf  47312  sge0fodjrnlem  47342  sge0iunmpt  47344  sge0rpcpnf  47347  nnfoctbdjlem  47381  meadjun  47388  voliunsge0lem  47398  hoicvr  47474  ovnn0val  47477  ovnsubaddlem1  47496  hoidmvn0val  47510  hsphoidmvle  47512  hoidmv1lelem1  47517  hoidmv1lelem2  47518  hoidmv1lelem3  47519  ovnhoilem1  47527  ovnsubadd2lem  47571  ovnovollem3  47584  cjnpoly  47855  lighneallem3  48608  divgcdoddALTV  48696  isubgr0uhgr  48887  usgrexmpl2trifr  49051  gpg5nbgrvtx03star  49094  gpg5nbgr3star  49095  smprngprmrng  49352  dignn0flhalflem1  49643  itcoval2  49692  itcoval3  49693  itcovalsuc  49695  ackvalsuc1mpt  49706  line2xlem  49781  nellindf  50886  veronesev1lem  50889  veronesev2lem  50890  veronesev3lem  50891  veronesev4lem  50892  veronesev5lem  50893  veronesev6lem  50894  veronesevrowd  50895