Theorem neneqd 2964

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1562   ≠ wne 2959

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 2960

This theorem is referenced by:  neneq  2965  necon2bi  2989  necon2i  2993  necon4i  2994  pm2.21ddne  3043  mteqand  3050  nelrdva  3670  eldifsnneq  4753  disjprg  5098  0inp0  5317  nelrnmpt  5945  rnmptn0  6233  resf1extb  7917  frxp2  8126  frxp3  8133  onnseq  8317  finnzfsuppd  9321  sniffsupp  9348  dfac2b  10089  ackbij1lem15  10191  ttukeylem7  10474  fpwwe2lem12  10602  canthnumlem  10608  canthp1lem2  10613  recgt0  12039  nnneneg  12250  elnnz  12580  xrnemnf  13121  xrnepnf  13122  fzprval  13592  fzodisjsn  13705  fzone1  13792  expnnval  14079  znsqcld  14177  hashelne0d  14383  elprchashprn2  14411  relexpsucnnr  15040  relexp1g  15041  relexpuzrel  15067  sgnp  15105  sgn0bi  15118  sgnmul  15122  fprodn0f  16023  ruclem12  16275  dvdsle  16346  nndvdslegcd  16541  gcdnncl  16543  divgcdnn  16551  nn0rppwr  16597  sqgcd  16598  eucalgf  16619  eucalginv  16620  lcmgcdlem  16642  lcmftp  16672  lcmfunsnlem2lem1  16674  lcmfunsnlem2lem2  16675  qredeu  16694  rpdvds  16696  cncongr2  16704  divnumden  16785  divdenle  16786  phisum  16828  oddprm  16848  pythagtriplem4  16857  pythagtriplem8  16861  pythagtriplem9  16862  4sqlem10  16985  ram0  17060  cat1lem  18131  isipodrs  18571  chnub  18656  chnpof1  18664  gsumval2  18722  smndex1n0mnd  18951  smndex2dnrinv  18954  mulgnn  19119  sylow1lem1  19640  gsumval3eu  19946  ablsimpgfindlem1  20151  ablsimpgfindlem2  20152  ablsimpgfind  20154  fincygsubgodd  20156  submomnd  20174  rrgnz  20756  fidomndrng  20825  abvtrivd  20883  ornglmullt  20920  orngrmullt  20921  suborng  20927  00lss  21010  lvecvscan2  21184  prmirredlem  21526  ofldchr  21630  uvcff  21845  mvrcl  22045  mplmon  22090  mplmonmul  22091  psdmul  22233  coe1tmfv2  22340  cply1coe0  22366  cply1coe0bi  22367  1marepvsma1  22645  mdetrsca2  22666  mdetrlin2  22669  mdetunilem2  22675  mdetunilem5  22678  mdetunilem6  22679  mdetunilem9  22682  maducoeval2  22702  gsummatr01lem3  22719  gsummatr01lem4  22720  gsummatr01  22721  m2cpm  22803  m2cpminvid2lem  22816  fvmptnn04ifa  22912  fvmptnn04ifb  22913  fvmptnn04ifc  22914  chfacffsupp  22918  chfacfscmul0  22920  chfacfscmulgsum  22922  chfacfpmmul0  22924  chfacfpmmulgsum  22926  connclo  23477  dissnlocfin  23591  ptpjpre2  23642  txindis  23696  snfil  23926  alexsublem  24106  tsmsfbas  24190  stdbdxmet  24577  dscmet  24634  xrsxmet  24872  iccpnfcnv  25008  cphsubrglem  25241  minveclem3b  25492  minveclem4a  25494  ovolicc1  25580  dvexp2  26018  dvmptdiv  26038  lhop2  26079  deg1sublt  26172  ig1pval3  26240  dvply1  26350  plydiveu  26364  quotcan  26375  aaliou3lem9  26416  taylthlem2  26439  pserdvlem2  26493  abelthlem9  26505  logccne0  26645  logtayllem  26726  logtayl  26727  cxpef  26732  rtprmirr  26827  angrtmuld  26875  isosctrlem3  26887  chordthmlem  26899  leibpilem2  27008  leibpi  27009  rlimcnp2  27033  efrlim  27036  vma1  27232  muinv  27259  lgsval2lem  27373  lgsval4  27383  lgsdir  27398  lgseisenlem4  27444  lgsquadlem1  27446  lgsquad2  27452  m1lgs  27454  2sqlem8a  27491  2sqlem8  27492  2sqcoprm  27501  2sqmod  27502  padicabv  27696  ostth1  27699  ostth3  27704  nolesgn2ores  27738  nogesgn1ores  27740  nosep1o  27747  nosep2o  27748  nosepdmlem  27749  nosepssdm  27752  noresle  27763  nosupbnd1lem3  27776  nosupbnd1lem4  27777  nosupbnd1lem5  27778  nosupbnd1lem6  27779  nosupbnd2lem1  27781  noinfbnd1lem3  27791  noinfbnd1lem4  27792  noinfbnd1lem5  27793  noinfbnd1lem6  27794  noinfbnd2lem1  27796  0elold  28005  elnnzs  28496  expnnsval  28521  expsne0  28531  bdayfinbndlem1  28562  tgbtwnne  28661  tgbtwndiff  28677  tgcolg  28725  tgbtwnconn1lem3  28745  legso  28770  tglineeltr  28802  tglineintmo  28813  tglineneq  28816  colline  28821  tglnpt4  28826  mirne  28842  miriso  28845  mirhl  28854  mirbtwnhl  28855  symquadlem  28864  krippenlem  28865  midexlem  28867  ragncol  28884  footexALT  28893  footexlem2  28895  colperp  28904  colperpexlem3  28907  mideulem2  28909  opphllem  28910  midex  28912  opptgdim2  28920  oppperpex  28928  hlpasch  28931  colopp  28944  lmieu  28959  trgcopy  28979  lnincplng  28993  plngrotlem1  28996  plngrotlem2  28997  lnssplnglem  29000  lnssplng  29001  cgracol  29024  cgrg3col4  29049  axlowdimlem15  29159  axcontlem2  29168  axcontlem7  29173  1egrvtxdg0  29714  2pthnloop  29933  cyclnspth  30003  eupth2lem1  30422  eupth2lem2  30423  eupth2lem3lem6  30437  nrt2irr  30677  strlem6  32461  hstrlem6  32469  atssma  32583  chirredlem1  32595  snsssng  32715  ifnetrue  32748  ifnefals  32749  fmptunsnop  32904  xaddeq0  32957  rexmul2  32958  xlt2addrd  32963  xnn0nn0d  32976  hashpss  33013  elq2  33016  divnumden2  33020  2exple2exp  33038  pmtridf1o  33276  pmtridfv1  33277  pmtridfv2  33278  elrgspnlem2  33426  elrgspnlem3  33427  domnprodeq0  33462  fracfld  33497  pidlnz  33564  lindssn  33566  drngidl  33621  drngidlhash  33622  0ringprmidl  33638  qsidomlem1  33641  ssdifidlprm  33647  mxidlmaxv  33658  mxidlprm  33660  mxidlirredi  33661  mxidlirred  33662  krull  33669  drnglring  33690  dflring3  33695  dflring4  33696  rsprprmprmidlb  33721  rprmasso2  33724  pidufd  33741  1arithufdlem3  33744  dfufd2  33748  zringidom  33749  0ringmon1p  33755  ig1pnunit  33799  mplmulmvr  33838  psrmonmul  33849  esplyfval2  33864  esplymhp  33867  esplyfval3  33871  vietadeg1  33877  lindsunlem  33923  fldextrspundgdvdslem  33979  fldext2rspun  33981  ply1annnr  34002  fldext2chn  34027  constrextdg2lem  34047  constrext2chnlem  34049  constrcon  34073  2sqr3minply  34079  cos9thpiminply  34087  1smat1  34103  submatminr1  34109  madjusmdetlem2  34127  zarcls1  34168  zarclsint  34171  zarclssn  34172  xrge0iifcnv  34232  xrge0iifcv  34233  xrge0iif1  34237  qqhval2lem  34280  qqhf  34285  qqhre  34319  esumrnmpt2  34367  esumcvgre  34390  inelpisys  34453  carsgclctunlem2  34618  ballotlemirc  34831  signswlid  34855  repr0  34907  reprlt  34915  reprgt  34917  reprinfz1  34918  tgoldbachgtda  34957  tgoldbachgt  34959  bnj1523  35368  acycgr2v  35505  fmlaomn0  35745  fmlasucdisj  35754  fz0n  36086  dfrdg2  36148  dfrdg4  36306  broutsideof2  36477  outsidele  36487  rankeq1o  36526  ivthALT  36700  limsucncmpi  36810  mh-inf3sn  36907  qdiff  37824  topdifinffinlem  37846  icorempo  37850  finxpreclem2  37889  finxp1o  37891  finxpreclem6  37895  poimirlem9  38133  poimirlem11  38135  poimirlem12  38136  poimirlem25  38149  fdc  38249  heibor1lem  38313  heiborlem4  38318  heiborlem6  38320  disjressuc2  38915  2atm  40156  lhpocnle  40645  lhp2at0nle  40664  trlval3  40816  cdleme18c  40922  cdlemg17b  41291  cdlemg17i  41298  dia2dimlem2  41694  dia2dimlem3  41695  dihord6apre  41885  dihatlat  41963  dochshpsat  42083  lcfrlem9  42179  mapdhval2  42355  hdmap1val2  42429  hdmap14lem4a  42500  hdmap14lem6  42502  dvrelogpow2b  42690  aks4d1p1p4  42693  aks4d1p6  42703  fldhmf1  42712  primrootspoweq0  42728  aks6d1c2p2  42741  hashscontpow  42744  aks6d1c5  42761  sticksstones1  42768  sticksstones10  42777  sticksstones12a  42779  sticksstones12  42780  sticksstones22  42790  aks6d1c6lem4  42795  aks6d1c7lem1  42802  aks6d1c7  42806  aks5lem8  42823  negn0nposznnd  42896  mhpind  43181  prjspner1  43213  dffltz  43221  3cubeslem2  43271  jm2.26lem3  43583  kelac1  43645  cantnfresb  43906  tfsconcat0b  43928  nlimsuc  44022  clsk1indlem0  44622  scotteld  44827  sineq0ALT  45517  refsum2cnlem1  45622  disjxp1  45654  disjf1  45766  disjrnmpt2  45771  disjinfi  45775  oddfl  45862  xrlttri5d  45868  supxrge  45919  nepnfltpnf  45923  nemnftgtmnft  45925  xrlexaddrp  45933  xrred  45945  supminfxr2  46048  icoiccdif  46105  qinioo  46116  ioonct  46118  fmul01lt1lem1  46165  climrec  46184  limcperiod  46209  reclimc  46232  limsupub  46283  liminflbuz2  46394  cncfiooicclem1  46472  cncfioobdlem  46475  fperdvper  46498  dvdivbd  46502  ditgeqiooicc  46539  itgsincmulx  46553  itgioocnicc  46556  iblcncfioo  46557  stoweidlem35  46614  stoweidlem39  46618  stirlinglem5  46657  stirlinglem8  46660  dirkerper  46675  dirkercncflem2  46683  dirkercncflem4  46685  fourierdlem31  46717  fourierdlem34  46720  fourierdlem41  46727  fourierdlem42  46728  fourierdlem44  46730  fourierdlem48  46733  fourierdlem49  46734  fourierdlem53  46738  fourierdlem56  46741  fourierdlem58  46743  fourierdlem60  46745  fourierdlem61  46746  fourierdlem62  46747  fourierdlem65  46750  fourierdlem66  46751  fourierdlem73  46758  fourierdlem76  46761  fourierdlem79  46764  fourierdlem81  46766  fourierdlem82  46767  fourierdlem93  46778  fourierdlem103  46788  fourierdlem104  46789  sqwvfoura  46807  fourierswlem  46809  elaa2lem  46812  elaa2  46813  etransclem4  46817  etransclem24  46837  etransclem31  46844  etransclem32  46845  etransclem35  46848  sge0repnf  46965  sge0fodjrnlem  46995  sge0iunmpt  46997  sge0rpcpnf  47000  nnfoctbdjlem  47034  meadjun  47041  voliunsge0lem  47051  hoicvr  47127  ovnn0val  47130  ovnsubaddlem1  47149  hoidmvn0val  47163  hsphoidmvle  47165  hoidmv1lelem1  47170  hoidmv1lelem2  47171  hoidmv1lelem3  47172  ovnhoilem1  47180  ovnsubadd2lem  47224  ovnovollem3  47237  cjnpoly  47488  lighneallem3  48221  divgcdoddALTV  48309  isubgr0uhgr  48500  usgrexmpl2trifr  48664  gpg5nbgrvtx03star  48707  gpg5nbgr3star  48708  dignn0flhalflem1  49242  itcoval2  49291  itcoval3  49292  itcovalsuc  49294  ackvalsuc1mpt  49305  line2xlem  49380