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  7935  frxp2  8146  frxp3  8153  onnseq  8337  finnzfsuppd  9347  sniffsupp  9374  scotteld  9890  dfac2b  10137  ackbij1lem15  10239  ttukeylem7  10521  fpwwe2lem12  10655  canthnumlem  10661  canthp1lem2  10666  recgt0  12089  nnneneg  12299  elnnz  12629  xrnemnf  13172  xrnepnf  13173  fzprval  13644  fzodisjsn  13757  fzone1  13844  expnnval  14132  znsqcld  14230  hashelne0d  14436  elprchashprn2  14464  hashpss  14478  relexpsucnnr  15102  relexp1g  15103  relexpuzrel  15129  sgnp  15167  sgn0bi  15180  sgnmul  15184  fprodn0f  16084  ruclem12  16335  dvdsle  16406  nndvdslegcd  16601  gcdnncl  16603  divgcdnn  16611  nn0rppwr  16657  sqgcd  16658  eucalgf  16679  eucalginv  16680  lcmgcdlem  16702  lcmftp  16732  lcmfunsnlem2lem1  16734  lcmfunsnlem2lem2  16735  qredeu  16754  rpdvds  16756  cncongr2  16764  divnumden  16845  divdenle  16846  phisum  16888  oddprm  16908  pythagtriplem4  16917  pythagtriplem8  16921  pythagtriplem9  16922  4sqlem10  17045  ram0  17120  cat1lem  18191  isipodrs  18631  chnub  18716  chnpof1  18724  gsumval2  18794  smndex1n0mnd  19030  smndex2dnrinv  19033  mulgnn  19204  sylow1lem1  19731  gsumval3eu  20037  ablsimpgfindlem1  20242  ablsimpgfindlem2  20243  ablsimpgfind  20245  fincygsubgodd  20247  submomnd  20265  rrgnz  20872  fidomndrng  20946  abvtrivd  21004  ornglmullt  21041  orngrmullt  21042  suborng  21048  00lss  21131  lvecvscan2  21305  pidlnz  21443  drngidl  21454  0ringprmidl  21546  qsidomlem1  21549  ssdifidlprm  21555  prmirredlem  21691  ofldchr  21795  uvcff  22010  mvrcl  22212  mplmon  22257  mplmonmul  22258  psdmul  22400  coe1tmfv2  22507  cply1coe0  22532  cply1coe0bi  22533  1marepvsma1  22811  mdetrsca2  22832  mdetrlin2  22835  mdetunilem2  22841  mdetunilem5  22844  mdetunilem6  22845  mdetunilem9  22848  maducoeval2  22868  gsummatr01lem3  22885  gsummatr01lem4  22886  gsummatr01  22887  m2cpm  22972  m2cpminvid2lem  22985  fvmptnn04ifa  23081  fvmptnn04ifb  23082  fvmptnn04ifc  23083  chfacffsupp  23087  chfacfscmul0  23089  chfacfscmulgsum  23091  chfacfpmmul0  23093  chfacfpmmulgsum  23095  connclo  23646  dissnlocfin  23761  ptpjpre2  23812  txindis  23866  snfil  24096  alexsublem  24276  tsmsfbas  24360  stdbdxmet  24747  dscmet  24804  xrsxmet  25042  iccpnfcnv  25178  cphsubrglem  25411  minveclem3b  25662  minveclem4a  25664  ovolicc1  25750  dvexp2  26188  dvmptdiv  26208  lhop2  26249  deg1sublt  26342  ig1pval3  26410  dvply1  26521  plydiveu  26535  rnplynfin  26546  quotcan  26548  aaliou3lem9  26593  taylthlem2  26617  pserdvlem2  26671  abelthlem9  26683  logccne0  26823  logtayllem  26904  logtayl  26905  cxpef  26910  rtprmirr  27005  angrtmuld  27053  isosctrlem3  27065  chordthmlem  27077  leibpilem2  27186  leibpi  27187  rlimcnp2  27211  efrlim  27214  vma1  27410  muinv  27437  lgsval2lem  27551  lgsval4  27561  lgsdir  27576  lgseisenlem4  27622  lgsquadlem1  27624  lgsquad2  27630  m1lgs  27632  2sqlem8a  27669  2sqlem8  27670  2sqcoprm  27679  2sqmod  27680  padicabv  27874  ostth1  27877  ostth3  27882  nolesgn2ores  27916  nogesgn1ores  27918  nosep1o  27925  nosep2o  27926  nosepdmlem  27927  nosepssdm  27930  noresle  27941  nosupbnd1lem3  27954  nosupbnd1lem4  27955  nosupbnd1lem5  27956  nosupbnd1lem6  27957  nosupbnd2lem1  27959  noinfbnd1lem3  27969  noinfbnd1lem4  27970  noinfbnd1lem5  27971  noinfbnd1lem6  27972  noinfbnd2lem1  27974  0elold  28183  elnnzs  28674  expnnsval  28699  expsne0  28709  bdayfinbndlem1  28740  tgbtwnne  28840  tgbtwndiff  28856  tgcolg  28904  tgbtwnconn1lem3  28924  legso  28949  tglineeltr  28986  tglineintmo  28997  tglineneq  29000  colline  29005  tglnpt4  29010  mirne  29026  miriso  29029  mirhl  29038  mirbtwnhl  29039  symquadlem  29048  krippenlem  29049  midexlem  29051  symquadprlnglem  29052  ragncol  29071  footexALT  29080  footexlem2  29082  colperp  29092  colperpexlem3  29095  mideulem2  29097  opphllem  29098  midex  29100  opptgdim2  29108  oppperpex  29116  hlpasch  29121  colopp  29134  lnincplng  29149  plngrotlem1  29152  plngrotlem2  29153  lnssplnglem  29156  lnssplng  29157  lmieu  29176  trgcopy  29198  cgracol  29223  tgaaddcpbllem1  29236  tgaaddcpbl  29239  tgaaddcpbl2  29240  cgrg3col4  29259  angmgmaddeu1  29266  angmgmaddov2lem  29274  angmgmaddcpbl  29277  prlngin0  29309  prlngpln  29310  prlnghpg  29311  dfprlng2  29312  prlngex  29316  prlngmolem1  29317  prlngmolem2  29318  prlngmo2  29321  prlngpln4  29323  prlnginn0  29325  prlngmid2  29326  prlngsymquadlem  29328  tgaltai  29332  axlowdimlem15  29421  axcontlem2  29430  axcontlem7  29435  1egrvtxdg0  29979  2pthnloop  30204  cyclnspth  30276  eupth2lem1  30706  eupth2lem2  30707  eupth2lem3lem6  30721  nrt2irr  30961  strlem6  32745  hstrlem6  32753  atssma  32867  chirredlem1  32879  snsssng  32997  ifnetrue  33030  ifnefals  33031  fmptunsnop  33180  xaddeq0  33232  rexmul2  33233  xlt2addrd  33238  xnn0nn0d  33251  elq2  33290  divnumden2  33294  2exple2exp  33312  pmtridf1o  33542  pmtridfv1  33543  pmtridfv2  33544  elrgspnlem2  33691  elrgspnlem3  33692  domnprodeq0  33727  fracfld  33757  lindssn  33819  drngidlhash  33869  mxidlmaxv  33879  mxidlprm  33881  mxidlirredi  33882  mxidlirred  33883  krull  33889  drnglring  33910  dflring3  33915  dflring4  33916  rsprprmprmidlb  33941  rprmasso2  33944  pidufd  33961  1arithufdlem3  33964  dfufd2  33968  zringidom  33969  0ringmon1p  33975  ig1pnunit  34019  mplmulmvr  34057  psrmonmul  34068  esplyfval2  34083  esplymhp  34086  esplyfval3  34090  vietadeg1  34096  lindsunlem  34142  fldextrspundgdvdslem  34198  fldext2rspun  34200  ply1annnr  34221  fldext2chn  34246  constrextdg2lem  34266  constrext2chnlem  34268  constrcon  34292  2sqr3minply  34298  cos9thpiminply  34306  1smat1  34322  submatminr1  34328  madjusmdetlem2  34346  zarcls1  34387  zarclsint  34390  zarclssn  34391  xrge0iifcnv  34451  xrge0iifcv  34452  xrge0iif1  34456  qqhval2lem  34499  qqhf  34504  qqhre  34538  esumrnmpt2  34586  esumcvgre  34609  inelpisys  34673  carsgclctunlem2  34838  ballotlemirc  35051  signswlid  35075  repr0  35127  reprlt  35135  reprgt  35137  reprinfz1  35138  tgoldbachgtda  35177  tgoldbachgt  35179  bnj1523  35588  kard0b  35693  acycgr2v  35737  fmlaomn0  35977  fmlasucdisj  35986  fz0n  36318  dfrdg2  36380  dfrdg4  36538  broutsideof2  36710  outsidele  36720  rankeq1o  36759  ivthALT  36962  limsucncmpi  37072  mh-inf3sn  37169  qdiff  38087  topdifinffinlem  38109  icorempo  38113  finxpreclem2  38152  finxp1o  38154  finxpreclem6  38158  poimirlem9  38386  poimirlem11  38388  poimirlem12  38389  poimirlem25  38402  fdc  38503  heibor1lem  38567  heiborlem4  38572  heiborlem6  38574  disjressuc2  39167  2atm  40408  lhpocnle  40897  lhp2at0nle  40916  trlval3  41068  cdleme18c  41174  cdlemg17b  41543  cdlemg17i  41550  dia2dimlem2  41946  dia2dimlem3  41947  dihord6apre  42137  dihatlat  42215  dochshpsat  42335  lcfrlem9  42431  mapdhval2  42607  hdmap1val2  42681  hdmap14lem4a  42752  hdmap14lem6  42754  dvrelogpow2b  42942  aks4d1p1p4  42945  aks4d1p6  42955  fldhmf1  42964  primrootspoweq0  42980  aks6d1c2p2  42993  hashscontpow  42996  aks6d1c5  43013  sticksstones1  43020  sticksstones10  43029  sticksstones12a  43031  sticksstones12  43032  sticksstones22  43042  aks6d1c6lem4  43047  aks6d1c7lem1  43054  aks6d1c7  43058  aks5lem8  43075  quadfac  43079  negn0nposznnd  43165  mhpind  43448  prjspner1  43480  dffltz  43488  3cubeslem2  43538  jm2.26lem3  43850  kelac1  43912  cantnfresb  44173  tfsconcat0b  44195  nlimsuc  44289  clsk1indlem0  44889  sineq0ALT  45767  refsum2cnlem1  45879  disjxp1  45911  disjf1  46023  disjrnmpt2  46028  disjinfi  46032  oddfl  46119  xrlttri5d  46125  supxrge  46176  nepnfltpnf  46180  nemnftgtmnft  46182  xrlexaddrp  46190  xrred  46202  supminfxr2  46305  icoiccdif  46362  qinioo  46373  ioonct  46375  fmul01lt1lem1  46422  climrec  46441  limcperiod  46466  reclimc  46489  limsupub  46540  liminflbuz2  46651  cncfiooicclem1  46729  cncfioobdlem  46732  fperdvper  46755  dvdivbd  46759  ditgeqiooicc  46796  itgsincmulx  46810  itgioocnicc  46813  iblcncfioo  46814  stoweidlem35  46871  stoweidlem39  46875  stirlinglem5  46914  stirlinglem8  46917  dirkerper  46932  dirkercncflem2  46940  dirkercncflem4  46942  fourierdlem31  46974  fourierdlem34  46977  fourierdlem41  46984  fourierdlem42  46985  fourierdlem44  46987  fourierdlem48  46990  fourierdlem49  46991  fourierdlem53  46995  fourierdlem56  46998  fourierdlem58  47000  fourierdlem60  47002  fourierdlem61  47003  fourierdlem62  47004  fourierdlem65  47007  fourierdlem66  47008  fourierdlem73  47015  fourierdlem76  47018  fourierdlem79  47021  fourierdlem81  47023  fourierdlem82  47024  fourierdlem93  47035  fourierdlem103  47045  fourierdlem104  47046  sqwvfoura  47064  fourierswlem  47066  elaa2lem  47069  elaa2  47070  etransclem4  47074  etransclem24  47094  etransclem31  47101  etransclem32  47102  etransclem35  47105  sge0repnf  47222  sge0fodjrnlem  47252  sge0iunmpt  47254  sge0rpcpnf  47257  nnfoctbdjlem  47291  meadjun  47298  voliunsge0lem  47308  hoicvr  47384  ovnn0val  47387  ovnsubaddlem1  47406  hoidmvn0val  47420  hsphoidmvle  47422  hoidmv1lelem1  47427  hoidmv1lelem2  47428  hoidmv1lelem3  47429  ovnhoilem1  47437  ovnsubadd2lem  47481  ovnovollem3  47494  cjnpoly  47765  lighneallem3  48518  divgcdoddALTV  48606  isubgr0uhgr  48797  usgrexmpl2trifr  48961  gpg5nbgrvtx03star  49004  gpg5nbgr3star  49005  smprngprmrng  49262  dignn0flhalflem1  49553  itcoval2  49602  itcoval3  49603  itcovalsuc  49605  ackvalsuc1mpt  49616  line2xlem  49691  nellindf  50811  veronesev1lem  50814  veronesev2lem  50815  veronesev3lem  50816  veronesev4lem  50817  veronesev5lem  50818  veronesev6lem  50819  veronesevrowd  50820