Theorem neneqd 2962

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

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

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 2958

This theorem is used by:  neneq  2963  necon2bi  2987  necon2i  2991  necon4i  2992  pm2.21ddne  3041  mteqand  3048  nelrdva  3666  nrmod  3842  eldifsnneq  4757  disjprg  5103  0inp0  5327  nelrnmpt  5955  rnmptn0  6244  resf1extb  7934  frxp2  8145  frxp3  8152  onnseq  8336  finnzfsuppd  9346  sniffsupp  9373  scotteld  9889  dfac2b  10136  ackbij1lem15  10238  ttukeylem7  10520  fpwwe2lem12  10652  canthnumlem  10658  canthp1lem2  10663  recgt0  12086  nnneneg  12296  elnnz  12626  xrnemnf  13168  xrnepnf  13169  fzprval  13640  fzodisjsn  13753  fzone1  13840  expnnval  14128  znsqcld  14226  hashelne0d  14432  elprchashprn2  14460  hashpss  14474  relexpsucnnr  15098  relexp1g  15099  relexpuzrel  15125  sgnp  15163  sgn0bi  15176  sgnmul  15180  fprodn0f  16080  ruclem12  16331  dvdsle  16402  nndvdslegcd  16597  gcdnncl  16599  divgcdnn  16607  nn0rppwr  16653  sqgcd  16654  eucalgf  16675  eucalginv  16676  lcmgcdlem  16698  lcmftp  16728  lcmfunsnlem2lem1  16730  lcmfunsnlem2lem2  16731  qredeu  16750  rpdvds  16752  cncongr2  16760  divnumden  16841  divdenle  16842  phisum  16884  oddprm  16904  pythagtriplem4  16913  pythagtriplem8  16917  pythagtriplem9  16918  4sqlem10  17041  ram0  17116  cat1lem  18187  isipodrs  18627  chnub  18712  chnpof1  18720  gsumval2  18788  smndex1n0mnd  19023  smndex2dnrinv  19026  mulgnn  19197  sylow1lem1  19724  gsumval3eu  20030  ablsimpgfindlem1  20235  ablsimpgfindlem2  20236  ablsimpgfind  20238  fincygsubgodd  20240  submomnd  20258  rrgnz  20865  fidomndrng  20939  abvtrivd  20997  ornglmullt  21034  orngrmullt  21035  suborng  21041  00lss  21124  lvecvscan2  21298  pidlnz  21436  drngidl  21447  0ringprmidl  21539  qsidomlem1  21542  ssdifidlprm  21548  prmirredlem  21684  ofldchr  21788  uvcff  22003  mvrcl  22205  mplmon  22250  mplmonmul  22251  psdmul  22393  coe1tmfv2  22500  cply1coe0  22525  cply1coe0bi  22526  1marepvsma1  22804  mdetrsca2  22825  mdetrlin2  22828  mdetunilem2  22834  mdetunilem5  22837  mdetunilem6  22838  mdetunilem9  22841  maducoeval2  22861  gsummatr01lem3  22878  gsummatr01lem4  22879  gsummatr01  22880  m2cpm  22965  m2cpminvid2lem  22978  fvmptnn04ifa  23074  fvmptnn04ifb  23075  fvmptnn04ifc  23076  chfacffsupp  23080  chfacfscmul0  23082  chfacfscmulgsum  23084  chfacfpmmul0  23086  chfacfpmmulgsum  23088  connclo  23639  dissnlocfin  23754  ptpjpre2  23805  txindis  23859  snfil  24089  alexsublem  24269  tsmsfbas  24353  stdbdxmet  24740  dscmet  24797  xrsxmet  25035  iccpnfcnv  25171  cphsubrglem  25404  minveclem3b  25655  minveclem4a  25657  ovolicc1  25743  dvexp2  26181  dvmptdiv  26201  lhop2  26242  deg1sublt  26335  ig1pval3  26403  dvply1  26513  plydiveu  26527  quotcan  26538  aaliou3lem9  26581  taylthlem2  26605  pserdvlem2  26659  abelthlem9  26671  logccne0  26811  logtayllem  26892  logtayl  26893  cxpef  26898  rtprmirr  26993  angrtmuld  27041  isosctrlem3  27053  chordthmlem  27065  leibpilem2  27174  leibpi  27175  rlimcnp2  27199  efrlim  27202  vma1  27398  muinv  27425  lgsval2lem  27539  lgsval4  27549  lgsdir  27564  lgseisenlem4  27610  lgsquadlem1  27612  lgsquad2  27618  m1lgs  27620  2sqlem8a  27657  2sqlem8  27658  2sqcoprm  27667  2sqmod  27668  padicabv  27862  ostth1  27865  ostth3  27870  nolesgn2ores  27904  nogesgn1ores  27906  nosep1o  27913  nosep2o  27914  nosepdmlem  27915  nosepssdm  27918  noresle  27929  nosupbnd1lem3  27942  nosupbnd1lem4  27943  nosupbnd1lem5  27944  nosupbnd1lem6  27945  nosupbnd2lem1  27947  noinfbnd1lem3  27957  noinfbnd1lem4  27958  noinfbnd1lem5  27959  noinfbnd1lem6  27960  noinfbnd2lem1  27962  0elold  28171  elnnzs  28662  expnnsval  28687  expsne0  28697  bdayfinbndlem1  28728  tgbtwnne  28828  tgbtwndiff  28844  tgcolg  28892  tgbtwnconn1lem3  28912  legso  28937  tglineeltr  28974  tglineintmo  28985  tglineneq  28988  colline  28993  tglnpt4  28998  mirne  29014  miriso  29017  mirhl  29026  mirbtwnhl  29027  symquadlem  29036  krippenlem  29037  midexlem  29039  symquadprlnglem  29040  ragncol  29059  footexALT  29068  footexlem2  29070  colperp  29080  colperpexlem3  29083  mideulem2  29085  opphllem  29086  midex  29088  opptgdim2  29096  oppperpex  29104  hlpasch  29109  colopp  29122  lnincplng  29137  plngrotlem1  29140  plngrotlem2  29141  lnssplnglem  29144  lnssplng  29145  lmieu  29164  trgcopy  29186  cgracol  29211  tgaaddcpbllem1  29224  tgaaddcpbl  29227  tgaaddcpbl2  29228  cgrg3col4  29247  angmndaddeu1  29250  angmndaddov2lem  29258  angmndaddcpbl  29261  prlngin0  29285  prlngpln  29286  prlnghpg  29287  dfprlng2  29288  prlngex  29292  prlngmolem1  29293  prlngmolem2  29294  prlngmo2  29297  prlngpln4  29299  prlnginn0  29301  prlngmid2  29302  prlngsymquadlem  29304  tgaltai  29308  axlowdimlem15  29397  axcontlem2  29406  axcontlem7  29411  1egrvtxdg0  29955  2pthnloop  30180  cyclnspth  30252  eupth2lem1  30682  eupth2lem2  30683  eupth2lem3lem6  30697  nrt2irr  30937  strlem6  32721  hstrlem6  32729  atssma  32843  chirredlem1  32855  snsssng  32973  ifnetrue  33006  ifnefals  33007  fmptunsnop  33157  xaddeq0  33209  rexmul2  33210  xlt2addrd  33215  xnn0nn0d  33228  elq2  33267  divnumden2  33271  2exple2exp  33289  pmtridf1o  33519  pmtridfv1  33520  pmtridfv2  33521  elrgspnlem2  33668  elrgspnlem3  33669  domnprodeq0  33704  fracfld  33734  lindssn  33796  drngidlhash  33846  mxidlmaxv  33856  mxidlprm  33858  mxidlirredi  33859  mxidlirred  33860  krull  33866  drnglring  33887  dflring3  33892  dflring4  33893  rsprprmprmidlb  33918  rprmasso2  33921  pidufd  33938  1arithufdlem3  33941  dfufd2  33945  zringidom  33946  0ringmon1p  33952  ig1pnunit  33996  mplmulmvr  34034  psrmonmul  34045  esplyfval2  34060  esplymhp  34063  esplyfval3  34067  vietadeg1  34073  lindsunlem  34119  fldextrspundgdvdslem  34175  fldext2rspun  34177  ply1annnr  34198  fldext2chn  34223  constrextdg2lem  34243  constrext2chnlem  34245  constrcon  34269  2sqr3minply  34275  cos9thpiminply  34283  1smat1  34299  submatminr1  34305  madjusmdetlem2  34323  zarcls1  34364  zarclsint  34367  zarclssn  34368  xrge0iifcnv  34428  xrge0iifcv  34429  xrge0iif1  34433  qqhval2lem  34476  qqhf  34481  qqhre  34515  esumrnmpt2  34563  esumcvgre  34586  inelpisys  34650  carsgclctunlem2  34815  ballotlemirc  35028  signswlid  35052  repr0  35104  reprlt  35112  reprgt  35114  reprinfz1  35115  tgoldbachgtda  35154  tgoldbachgt  35156  bnj1523  35565  kard0b  35670  acycgr2v  35714  fmlaomn0  35954  fmlasucdisj  35963  fz0n  36295  dfrdg2  36357  dfrdg4  36515  broutsideof2  36687  outsidele  36697  rankeq1o  36736  ivthALT  36939  limsucncmpi  37049  mh-inf3sn  37146  qdiff  38064  topdifinffinlem  38086  icorempo  38090  finxpreclem2  38129  finxp1o  38131  finxpreclem6  38135  poimirlem9  38363  poimirlem11  38365  poimirlem12  38366  poimirlem25  38379  fdc  38480  heibor1lem  38544  heiborlem4  38549  heiborlem6  38551  disjressuc2  39144  2atm  40385  lhpocnle  40874  lhp2at0nle  40893  trlval3  41045  cdleme18c  41151  cdlemg17b  41520  cdlemg17i  41527  dia2dimlem2  41923  dia2dimlem3  41924  dihord6apre  42114  dihatlat  42192  dochshpsat  42312  lcfrlem9  42408  mapdhval2  42584  hdmap1val2  42658  hdmap14lem4a  42729  hdmap14lem6  42731  dvrelogpow2b  42919  aks4d1p1p4  42922  aks4d1p6  42932  fldhmf1  42941  primrootspoweq0  42957  aks6d1c2p2  42970  hashscontpow  42973  aks6d1c5  42990  sticksstones1  42997  sticksstones10  43006  sticksstones12a  43008  sticksstones12  43009  sticksstones22  43019  aks6d1c6lem4  43024  aks6d1c7lem1  43031  aks6d1c7  43035  aks5lem8  43052  quadfac  43056  negn0nposznnd  43142  mhpind  43425  prjspner1  43457  dffltz  43465  3cubeslem2  43515  jm2.26lem3  43827  kelac1  43889  cantnfresb  44150  tfsconcat0b  44172  nlimsuc  44266  clsk1indlem0  44866  sineq0ALT  45744  refsum2cnlem1  45856  disjxp1  45888  disjf1  46000  disjrnmpt2  46005  disjinfi  46009  oddfl  46096  xrlttri5d  46102  supxrge  46153  nepnfltpnf  46157  nemnftgtmnft  46159  xrlexaddrp  46167  xrred  46179  supminfxr2  46282  icoiccdif  46339  qinioo  46350  ioonct  46352  fmul01lt1lem1  46399  climrec  46418  limcperiod  46443  reclimc  46466  limsupub  46517  liminflbuz2  46628  cncfiooicclem1  46706  cncfioobdlem  46709  fperdvper  46732  dvdivbd  46736  ditgeqiooicc  46773  itgsincmulx  46787  itgioocnicc  46790  iblcncfioo  46791  stoweidlem35  46848  stoweidlem39  46852  stirlinglem5  46891  stirlinglem8  46894  dirkerper  46909  dirkercncflem2  46917  dirkercncflem4  46919  fourierdlem31  46951  fourierdlem34  46954  fourierdlem41  46961  fourierdlem42  46962  fourierdlem44  46964  fourierdlem48  46967  fourierdlem49  46968  fourierdlem53  46972  fourierdlem56  46975  fourierdlem58  46977  fourierdlem60  46979  fourierdlem61  46980  fourierdlem62  46981  fourierdlem65  46984  fourierdlem66  46985  fourierdlem73  46992  fourierdlem76  46995  fourierdlem79  46998  fourierdlem81  47000  fourierdlem82  47001  fourierdlem93  47012  fourierdlem103  47022  fourierdlem104  47023  sqwvfoura  47041  fourierswlem  47043  elaa2lem  47046  elaa2  47047  etransclem4  47051  etransclem24  47071  etransclem31  47078  etransclem32  47079  etransclem35  47082  sge0repnf  47199  sge0fodjrnlem  47229  sge0iunmpt  47231  sge0rpcpnf  47234  nnfoctbdjlem  47268  meadjun  47275  voliunsge0lem  47285  hoicvr  47361  ovnn0val  47364  ovnsubaddlem1  47383  hoidmvn0val  47397  hsphoidmvle  47399  hoidmv1lelem1  47404  hoidmv1lelem2  47405  hoidmv1lelem3  47406  ovnhoilem1  47414  ovnsubadd2lem  47458  ovnovollem3  47471  cjnpoly  47742  lighneallem3  48495  divgcdoddALTV  48583  isubgr0uhgr  48774  usgrexmpl2trifr  48938  gpg5nbgrvtx03star  48981  gpg5nbgr3star  48982  smprngprmrng  49239  dignn0flhalflem1  49530  itcoval2  49579  itcoval3  49580  itcovalsuc  49582  ackvalsuc1mpt  49593  line2xlem  49668  nellindf  50785  veronesev1lem  50788  veronesev2lem  50789  veronesev3lem  50790  veronesev4lem  50791  veronesev5lem  50792  veronesev6lem  50793  veronesevrowd  50794