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 1569   ≠ 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  3662  nrmod  3838  eldifsnneq  4753  disjprg  5098  0inp0  5319  nelrnmpt  5948  rnmptn0  6245  resf1extb  7946  frxp2  8161  frxp3  8168  onnseq  8352  finnzfsuppd  9365  sniffsupp  9392  scotteld  9947  dfac2b  10209  ackbij1lem15  10311  ttukeylem7  10593  fpwwe2lem12  10727  canthnumlem  10733  canthp1lem2  10738  recgt0  12163  nnneneg  12373  elnnz  12703  xrnemnf  13246  xrnepnf  13247  fzprval  13719  fzodisjsn  13832  fzone1  13919  expnnval  14207  znsqcld  14305  hashelne0d  14512  elprchashprn2  14540  hashpss  14554  relexpsucnnr  15178  relexp1g  15179  relexpuzrel  15205  sgnp  15243  sgn0bi  15256  sgnmul  15260  fprodn0f  16158  ruclem12  16409  dvdsle  16480  nndvdslegcd  16675  gcdnncl  16677  divgcdnn  16687  nn0rppwr  16735  sqgcd  16736  eucalgf  16758  eucalginv  16759  lcmgcdlem  16781  lcmftp  16811  lcmfunsnlem2lem1  16813  lcmfunsnlem2lem2  16814  qredeu  16833  rpdvds  16835  cncongr2  16843  divnumden  16924  divdenle  16925  phisum  16968  oddprm  16988  pythagtriplem4  16997  pythagtriplem8  17001  pythagtriplem9  17002  4sqlem10  17125  ram0  17200  cat1lem  18271  isipodrs  18711  chnub  18796  chnpof1  18804  gsumval2  18875  smndex1n0mnd  19111  smndex2dnrinv  19114  mulgnn  19285  sylow1lem1  19812  gsumval3eu  20118  ablsimpgfindlem1  20323  ablsimpgfindlem2  20324  ablsimpgfind  20326  fincygsubgodd  20328  submomnd  20346  rrgnz  20956  fidomndrng  21031  abvtrivd  21089  ornglmullt  21126  orngrmullt  21127  suborng  21133  00lss  21216  lvecvscan2  21390  pidlnz  21528  drngidl  21539  0ringprmidl  21633  qsidomlem1  21636  ssdifidlprm  21642  prmirredlem  21778  ofldchr  21882  uvcff  22097  mvrcl  22299  mplmon  22344  mplmonmul  22345  psdmul  22487  coe1tmfv2  22594  cply1coe0  22619  cply1coe0bi  22620  1marepvsma1  22898  mdetrsca2  22919  mdetrlin2  22922  mdetunilem2  22928  mdetunilem5  22931  mdetunilem6  22932  mdetunilem9  22935  maducoeval2  22955  gsummatr01lem3  22972  gsummatr01lem4  22973  gsummatr01  22974  m2cpm  23059  m2cpminvid2lem  23072  fvmptnn04ifa  23168  fvmptnn04ifb  23169  fvmptnn04ifc  23170  chfacffsupp  23174  chfacfscmul0  23176  chfacfscmulgsum  23178  chfacfpmmul0  23180  chfacfpmmulgsum  23182  connclo  23733  dissnlocfin  23848  ptpjpre2  23899  txindis  23953  snfil  24183  alexsublem  24363  tsmsfbas  24447  stdbdxmet  24834  dscmet  24891  xrsxmet  25129  iccpnfcnv  25265  cphsubrglem  25498  minveclem3b  25749  minveclem4a  25751  ovolicc1  25837  dvexp2  26274  dvmptdiv  26294  lhop2  26335  deg1sublt  26428  ig1pval3  26496  dvply1  26605  plydiveu  26619  rnplynfin  26630  quotcan  26632  aaliou3lem9  26677  taylthlem2  26701  pserdvlem2  26755  abelthlem9  26767  logccne0  26906  logtayllem  26987  logtayl  26988  cxpef  26993  rtprmirr  27088  angrtmuld  27136  isosctrlem3  27148  chordthmlem  27160  leibpilem2  27269  leibpi  27270  rlimcnp2  27294  efrlim  27297  vma1  27493  muinv  27520  lgsval2lem  27634  lgsval4  27644  lgsdir  27659  lgseisenlem4  27705  lgsquadlem1  27707  lgsquad2  27713  m1lgs  27715  2sqlem8a  27752  2sqlem8  27753  2sqcoprm  27762  2sqmod  27763  padicabv  27957  ostth1  27960  ostth3  27965  flt4ALT  27992  nolesgn2ores  28029  nogesgn1ores  28031  nosep1o  28038  nosep2o  28039  nosepdmlem  28040  nosepssdm  28043  noresle  28054  nosupbnd1lem3  28067  nosupbnd1lem4  28068  nosupbnd1lem5  28069  nosupbnd1lem6  28070  nosupbnd2lem1  28072  noinfbnd1lem3  28082  noinfbnd1lem4  28083  noinfbnd1lem5  28084  noinfbnd1lem6  28085  noinfbnd2lem1  28087  0elold  28296  elnnzs  28787  expnnsval  28812  expsne0  28822  bdayfinbndlem1  28853  tgbtwnne  28953  tgbtwndiff  28969  tgcolg  29017  tgbtwnconn1lem3  29037  legso  29062  tglineeltr  29099  tglineintmo  29110  tglineneq  29113  colline  29118  tglnpt4  29123  mirne  29139  miriso  29142  mirhl  29151  mirbtwnhl  29152  symquadlem  29161  krippenlem  29162  midexlem  29164  symquadprlnglem  29165  ragncol  29184  footexALT  29193  footexlem2  29195  colperp  29205  colperpexlem3  29208  mideulem2  29210  opphllem  29211  midex  29213  opptgdim2  29221  oppperpex  29229  hlpasch  29234  colopp  29247  lnincplng  29262  plngrotlem1  29265  plngrotlem2  29266  lnssplnglem  29269  lnssplng  29270  lmieu  29289  trgcopy  29311  cgracol  29336  tgaaddcpbllem1  29349  tgaaddcpbl  29352  tgaaddcpbl2  29353  cgrg3col4  29372  angmgmaddeu1  29379  angmgmaddov2lem  29387  angmgmaddcpbl  29390  prlngin0  29422  prlngpln  29423  prlnghpg  29424  dfprlng2  29425  prlngex  29429  prlngmolem1  29430  prlngmolem2  29431  prlngmo2  29434  prlngpln4  29436  prlnginn0  29438  prlngmid2  29439  prlngsymquadlem  29441  tgaltai  29445  axlowdimlem15  29534  axcontlem2  29543  axcontlem7  29548  1egrvtxdg0  30092  2pthnloop  30317  cyclnspth  30389  eupth2lem1  30819  eupth2lem2  30820  eupth2lem3lem6  30834  nrt2irr  31074  strlem6  32858  hstrlem6  32866  atssma  32980  chirredlem1  32992  snsssng  33110  ifnetrue  33143  ifnefals  33144  fmptunsnop  33293  xaddeq0  33345  rexmul2  33346  xlt2addrd  33351  xnn0nn0d  33364  elq2  33403  divnumden2  33407  2exple2exp  33425  pmtridf1o  33655  pmtridfv1  33656  pmtridfv2  33657  elrgspnlem2  33804  elrgspnlem3  33805  domnprodeq0  33840  fracfld  33870  lindssn  33933  drngidlhash  33983  mxidlmaxv  33993  mxidlprm  33995  mxidlirredi  33996  mxidlirred  33997  krull  34003  drnglring  34024  dflring3  34029  dflring4  34030  rsprprmprmidlb  34055  rprmasso2  34058  pidufd  34075  1arithufdlem3  34078  dfufd2  34082  zringidom  34083  0ringmon1p  34089  ig1pnunit  34133  mplmulmvr  34171  psrmonmul  34182  esplyfval2  34197  esplymhp  34200  esplyfval3  34204  vietadeg1  34210  lindsunlem  34256  fldextrspundgdvdslem  34312  fldext2rspun  34314  ply1annnr  34335  fldext2chn  34360  constrextdg2lem  34380  constrext2chnlem  34382  constrcon  34406  2sqr3minply  34412  cos9thpiminply  34420  1smat1  34436  submatminr1  34442  madjusmdetlem2  34460  zarcls1  34501  zarclsint  34504  zarclssn  34505  xrge0iifcnv  34565  xrge0iifcv  34566  xrge0iif1  34570  qqhval2lem  34613  qqhf  34618  qqhre  34652  esumrnmpt2  34700  esumcvgre  34723  inelpisys  34787  carsgclctunlem2  34951  ballotlemirc  35164  signswlid  35188  repr0  35240  reprlt  35248  reprgt  35250  reprinfz1  35251  tgoldbachgtda  35290  tgoldbachgt  35292  bnj1523  35701  kard0b  35827  acycgr2v  35915  fmlaomn0  36155  fmlasucdisj  36164  fz0n  36496  dfrdg2  36557  dfrdg4  36715  broutsideof2  36887  outsidele  36897  rankeq1o  36932  ivthALT  37123  limsucncmpi  37233  mh-inf3sn  37330  qdiff  38249  topdifinffinlem  38271  icorempo  38275  finxpreclem2  38314  finxp1o  38316  finxpreclem6  38320  poimirlem9  38548  poimirlem11  38550  poimirlem12  38551  poimirlem25  38564  fdc  38680  heibor1lem  38744  heiborlem4  38749  heiborlem6  38751  disjressuc2  39344  2atm  40585  lhpocnle  41074  lhp2at0nle  41093  trlval3  41245  cdleme18c  41351  cdlemg17b  41720  cdlemg17i  41727  dia2dimlem2  42123  dia2dimlem3  42124  dihord6apre  42314  dihatlat  42392  dochshpsat  42512  lcfrlem9  42608  mapdhval2  42784  hdmap1val2  42858  hdmap14lem4a  42929  hdmap14lem6  42931  dvrelogpow2b  43119  aks4d1p1p4  43122  aks4d1p6  43132  fldhmf1  43141  primrootspoweq0  43157  aks6d1c2p2  43170  hashscontpow  43173  aks6d1c5  43190  sticksstones1  43197  sticksstones10  43206  sticksstones12a  43208  sticksstones12  43209  sticksstones22  43219  aks6d1c6lem4  43224  aks6d1c7lem1  43231  aks6d1c7  43235  aks5lem8  43252  quadfac  43256  negn0nposznnd  43340  mhpind  43623  frlmnzcoordex  43653  frlmnzcoordsca  43659  dffltz  43671  3cubeslem2  43696  jm2.26lem3  44008  kelac1  44065  cantnfresb  44326  tfsconcat0b  44348  nlimsuc  44442  clsk1indlem0  45041  sineq0ALT  45919  refsum2cnlem1  46054  disjxp1  46086  disjf1  46198  disjrnmpt2  46203  disjinfi  46207  oddfl  46294  xrlttri5d  46300  supxrge  46350  nepnfltpnf  46354  nemnftgtmnft  46356  xrlexaddrp  46364  xrred  46376  supminfxr2  46479  icoiccdif  46536  qinioo  46547  ioonct  46549  fmul01lt1lem1  46596  climrec  46615  limcperiod  46640  reclimc  46663  limsupub  46714  liminflbuz2  46825  cncfiooicclem1  46903  cncfioobdlem  46906  fperdvper  46929  dvdivbd  46933  ditgeqiooicc  46970  itgsincmulx  46984  itgioocnicc  46987  iblcncfioo  46988  stoweidlem35  47045  stoweidlem39  47049  stirlinglem5  47088  stirlinglem8  47091  dirkerper  47106  dirkercncflem2  47114  dirkercncflem4  47116  fourierdlem31  47148  fourierdlem34  47151  fourierdlem41  47158  fourierdlem42  47159  fourierdlem44  47161  fourierdlem48  47164  fourierdlem49  47165  fourierdlem53  47169  fourierdlem56  47172  fourierdlem58  47174  fourierdlem60  47176  fourierdlem61  47177  fourierdlem62  47178  fourierdlem65  47181  fourierdlem66  47182  fourierdlem73  47189  fourierdlem76  47192  fourierdlem79  47195  fourierdlem81  47197  fourierdlem82  47198  fourierdlem93  47209  fourierdlem103  47219  fourierdlem104  47220  sqwvfoura  47238  fourierswlem  47240  elaa2lem  47243  elaa2  47244  etransclem4  47248  etransclem24  47268  etransclem31  47275  etransclem32  47276  etransclem35  47279  sge0repnf  47396  sge0fodjrnlem  47426  sge0iunmpt  47428  sge0rpcpnf  47431  nnfoctbdjlem  47465  meadjun  47472  voliunsge0lem  47482  hoicvr  47558  ovnn0val  47561  ovnsubaddlem1  47580  hoidmvn0val  47594  hsphoidmvle  47596  hoidmv1lelem1  47601  hoidmv1lelem2  47602  hoidmv1lelem3  47603  ovnhoilem1  47611  ovnsubadd2lem  47655  ovnovollem3  47668  cjnpoly  47939  lighneallem3  48692  divgcdoddALTV  48780  isubgr0uhgr  48971  usgrexmpl2trifr  49135  gpg5nbgrvtx03star  49178  gpg5nbgr3star  49179  smprngprmrng  49436  dignn0flhalflem1  49727  itcoval2  49776  itcoval3  49777  itcovalsuc  49779  ackvalsuc1mpt  49790  line2xlem  49865  nellindf  50970  veronesev1lem  50973  veronesev2lem  50974  veronesev3lem  50975  veronesev4lem  50976  veronesev5lem  50977  veronesev6lem  50978  veronesevrowd  50979