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 221	1 ⊢ (𝜑 → ¬ 𝐴 = 𝐵)

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

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 2960

This theorem is used by:  neneq  2965  necon2bi  2989  necon2i  2993  necon4i  2994  pm2.21ddne  3043  mteqand  3050  nelrdva  3666  nrmod  3843  eldifsnneq  4754  disjprg  5102  0inp0  5324  nelrnmpt  5955  rnmptn0  6257  resf1extb  7967  frxp2  8185  frxp3  8192  onnseq  8377  finnzfsuppd  9389  sniffsupp  9416  scotteld  9971  dfac2b  10233  ackbij1lem15  10335  ttukeylem7  10617  fpwwe2lem12  10751  canthnumlem  10757  canthp1lem2  10762  recgt0  12187  nnneneg  12397  elnnz  12727  xrnemnf  13270  xrnepnf  13271  fzprval  13743  fzodisjsn  13856  fzone1  13943  expnnval  14231  znsqcld  14329  hashelne0d  14536  elprchashprn2  14564  hashpss  14578  relexpsucnnr  15204  relexp1g  15205  relexpuzrel  15231  sgnp  15269  sgn0bi  15282  sgnmul  15286  fprodn0f  16184  ruclem12  16435  dvdsle  16506  nndvdslegcd  16701  gcdnncl  16703  divgcdnn  16713  nn0rppwr  16761  sqgcd  16762  eucalgf  16784  eucalginv  16785  lcmgcdlem  16807  lcmftp  16837  lcmfunsnlem2lem1  16839  lcmfunsnlem2lem2  16840  qredeu  16859  rpdvds  16861  cncongr2  16869  divnumden  16950  divdenle  16951  phisum  16994  oddprm  17014  pythagtriplem4  17023  pythagtriplem8  17027  pythagtriplem9  17028  4sqlem10  17151  ram0  17226  cat1lem  18297  isipodrs  18737  chnub  18822  chnpof1  18830  gsumval2  18901  smndex1n0mnd  19137  smndex2dnrinv  19140  mulgnn  19311  sylow1lem1  19839  gsumval3eu  20145  ablsimpgfindlem1  20350  ablsimpgfindlem2  20351  ablsimpgfind  20353  fincygsubgodd  20355  submomnd  20373  rrgnz  20983  fidomndrng  21058  abvtrivd  21116  ornglmullt  21153  orngrmullt  21154  suborng  21160  00lss  21243  lvecvscan2  21417  pidlnz  21555  drngidl  21566  0ringprmidl  21660  qsidomlem1  21663  ssdifidlprm  21669  prmirredlem  21805  ofldchr  21909  uvcff  22124  mvrcl  22326  mplmon  22371  mplmonmul  22372  psdmul  22514  coe1tmfv2  22621  cply1coe0  22646  cply1coe0bi  22647  1marepvsma1  22925  mdetrsca2  22946  mdetrlin2  22949  mdetunilem2  22955  mdetunilem5  22958  mdetunilem6  22959  mdetunilem9  22962  maducoeval2  22982  gsummatr01lem3  22999  gsummatr01lem4  23000  gsummatr01  23001  m2cpm  23086  m2cpminvid2lem  23099  fvmptnn04ifa  23195  fvmptnn04ifb  23196  fvmptnn04ifc  23197  chfacffsupp  23201  chfacfscmul0  23203  chfacfscmulgsum  23205  chfacfpmmul0  23207  chfacfpmmulgsum  23209  connclo  23760  dissnlocfin  23875  ptpjpre2  23926  txindis  23980  snfil  24210  alexsublem  24390  tsmsfbas  24474  stdbdxmet  24861  dscmet  24918  xrsxmet  25156  iccpnfcnv  25292  cphsubrglem  25525  minveclem3b  25776  minveclem4a  25778  ovolicc1  25864  dvexp2  26301  dvmptdiv  26321  lhop2  26362  deg1sublt  26455  ig1pval3  26523  dvply1  26632  plydiveu  26646  rnplynfin  26657  quotcan  26659  aaliou3lem9  26704  taylthlem2  26728  pserdvlem2  26782  abelthlem9  26794  logccne0  26933  logtayllem  27014  logtayl  27015  cxpef  27020  rtprmirr  27115  angrtmuld  27163  isosctrlem3  27175  chordthmlem  27187  leibpilem2  27296  leibpi  27297  rlimcnp2  27321  efrlim  27324  vma1  27520  muinv  27547  lgsval2lem  27661  lgsval4  27671  lgsdir  27686  lgseisenlem4  27732  lgsquadlem1  27734  lgsquad2  27740  m1lgs  27742  2sqlem8a  27779  2sqlem8  27780  2sqcoprm  27789  2sqmod  27790  padicabv  27984  ostth1  27987  ostth3  27992  flt4ALT  28019  nolesgn2ores  28056  nogesgn1ores  28058  nosep1o  28065  nosep2o  28066  nosepdmlem  28067  nosepssdm  28070  noresle  28081  nosupbnd1lem3  28094  nosupbnd1lem4  28095  nosupbnd1lem5  28096  nosupbnd1lem6  28097  nosupbnd2lem1  28099  noinfbnd1lem3  28109  noinfbnd1lem4  28110  noinfbnd1lem5  28111  noinfbnd1lem6  28112  noinfbnd2lem1  28114  0elold  28323  elnnzs  28814  expnnsval  28839  expsne0  28849  bdayfinbndlem1  28880  tgbtwnne  28980  tgbtwndiff  28996  tgcolg  29044  tgbtwnconn1lem3  29064  legso  29089  tglineeltr  29126  tglineintmo  29137  tglineneq  29140  colline  29145  tglnpt4  29150  mirne  29166  miriso  29169  mirhl  29178  mirbtwnhl  29179  symquadlem  29188  krippenlem  29189  midexlem  29191  symquadprlnglem  29192  ragncol  29211  footexALT  29220  footexlem2  29222  colperp  29232  colperpexlem3  29235  mideulem2  29237  opphllem  29238  midex  29240  opptgdim2  29248  oppperpex  29256  hlpasch  29261  colopp  29274  lnincplng  29289  plngrotlem1  29292  plngrotlem2  29293  lnssplnglem  29296  lnssplng  29297  lmieu  29316  trgcopy  29338  cgracol  29363  tgaaddcpbllem1  29376  tgaaddcpbl  29379  tgaaddcpbl2  29380  cgrg3col4  29399  angmgmaddeu1  29406  angmgmaddov2lem  29414  angmgmaddcpbl  29417  prlngin0  29449  prlngpln  29450  prlnghpg  29451  dfprlng2  29452  prlngex  29456  prlngmolem1  29457  prlngmolem2  29458  prlngmo2  29461  prlngpln4  29463  prlnginn0  29465  prlngmid2  29466  prlngsymquadlem  29468  tgaltai  29472  axlowdimlem15  29561  axcontlem2  29570  axcontlem7  29575  1egrvtxdg0  30119  2pthnloop  30344  cyclnspth  30416  eupth2lem1  30846  eupth2lem2  30847  eupth2lem3lem6  30861  nrt2irr  31101  strlem6  32885  hstrlem6  32893  atssma  33007  chirredlem1  33019  inagcgrabtwn  33078  cgrainag  33087  tgextamirn  33094  tgextancd  33095  tgextamirnhl  33099  tgaasncol  33107  snsssng  33179  ifnetrue  33212  ifnefals  33213  fmptunsnop  33361  xaddeq0  33412  rexmul2  33413  xlt2addrd  33418  xnn0nn0d  33431  elq2  33470  divnumden2  33474  2exple2exp  33492  pmtridf1o  33722  pmtridfv1  33723  pmtridfv2  33724  elrgspnlem2  33871  elrgspnlem3  33872  domnprodeq0  33907  fracfld  33937  lindssn  34000  drngidlhash  34050  mxidlmaxv  34060  mxidlprm  34062  mxidlirredi  34063  mxidlirred  34064  krull  34070  drnglring  34091  dflring3  34096  dflring4  34097  rsprprmprmidlb  34122  rprmasso2  34125  pidufd  34142  1arithufdlem3  34145  dfufd2  34149  zringidom  34150  0ringmon1p  34156  ig1pnunit  34200  mplmulmvr  34238  psrmonmul  34249  esplyfval2  34264  esplymhp  34267  esplyfval3  34271  vietadeg1  34277  lindsunlem  34323  fldextrspundgdvdslem  34379  fldext2rspun  34381  ply1annnr  34402  fldext2chn  34427  constrextdg2lem  34447  constrext2chnlem  34449  constrcon  34473  2sqr3minply  34479  cos9thpiminply  34487  1smat1  34503  submatminr1  34509  madjusmdetlem2  34527  zarcls1  34568  zarclsint  34571  zarclssn  34572  xrge0iifcnv  34632  xrge0iifcv  34633  xrge0iif1  34637  qqhval2lem  34680  qqhf  34685  qqhre  34719  esumrnmpt2  34767  esumcvgre  34790  inelpisys  34854  carsgclctunlem2  35018  ballotlemirc  35231  signswlid  35255  repr0  35307  reprlt  35315  reprgt  35317  reprinfz1  35318  tgoldbachgtda  35357  tgoldbachgt  35359  bnj1523  35768  0elscott  35836  ecscottd  35843  kard0b  35926  fnlfvk3n0  36027  acycgr2v  36071  fmlaomn0  36321  fmlasucdisj  36330  fz0n  36673  dfrdg2  36734  dfrdg4  36892  broutsideof2  37064  outsidele  37074  rankeq1o  37109  ivthALT  37300  limsucncmpi  37410  mh-inf3sn  37507  qdiff  38439  topdifinffinlem  38461  icorempo  38465  finxpreclem2  38504  finxp1o  38506  finxpreclem6  38510  poimirlem9  38738  poimirlem11  38740  poimirlem12  38741  poimirlem25  38754  fdc  38870  heibor1lem  38934  heiborlem4  38939  heiborlem6  38941  disjressuc2  39534  2atm  40775  lhpocnle  41264  lhp2at0nle  41283  trlval3  41435  cdleme18c  41541  cdlemg17b  41910  cdlemg17i  41917  dia2dimlem2  42313  dia2dimlem3  42314  dihord6apre  42504  dihatlat  42582  dochshpsat  42702  lcfrlem9  42798  mapdhval2  42974  hdmap1val2  43048  hdmap14lem4a  43119  hdmap14lem6  43121  dvrelogpow2b  43309  aks4d1p1p4  43312  aks4d1p6  43322  fldhmf1  43331  primrootspoweq0  43347  aks6d1c2p2  43360  hashscontpow  43363  aks6d1c5  43380  sticksstones1  43387  sticksstones10  43396  sticksstones12a  43398  sticksstones12  43399  sticksstones22  43409  aks6d1c6lem4  43414  aks6d1c7lem1  43421  aks6d1c7  43425  aks5lem8  43442  quadfac  43446  negn0nposznnd  43530  mhpind  43813  frlmnzcoordex  43843  frlmnzcoordsca  43849  dffltz  43861  3cubeslem2  43886  jm2.26lem3  44199  kelac1  44256  cantnfresb  44516  tfsconcat0b  44538  nlimsuc  44632  clsk1indlem0  45231  sineq0ALT  46108  refsum2cnlem1  46257  disjxp1  46289  disjf1  46401  disjrnmpt2  46406  disjinfi  46410  oddfl  46497  xrlttri5d  46503  supxrge  46553  nepnfltpnf  46557  nemnftgtmnft  46559  xrlexaddrp  46567  xrred  46579  supminfxr2  46682  icoiccdif  46739  qinioo  46750  ioonct  46752  fmul01lt1lem1  46799  climrec  46818  limcperiod  46843  reclimc  46866  limsupub  46917  liminflbuz2  47028  cncfiooicclem1  47106  cncfioobdlem  47109  fperdvper  47132  dvdivbd  47136  ditgeqiooicc  47173  itgsincmulx  47187  itgioocnicc  47190  iblcncfioo  47191  stoweidlem35  47248  stoweidlem39  47252  stirlinglem5  47291  stirlinglem8  47294  dirkerper  47309  dirkercncflem2  47317  dirkercncflem4  47319  fourierdlem31  47351  fourierdlem34  47354  fourierdlem41  47361  fourierdlem42  47362  fourierdlem44  47364  fourierdlem48  47367  fourierdlem49  47368  fourierdlem53  47372  fourierdlem56  47375  fourierdlem58  47377  fourierdlem60  47379  fourierdlem61  47380  fourierdlem62  47381  fourierdlem65  47384  fourierdlem66  47385  fourierdlem73  47392  fourierdlem76  47395  fourierdlem79  47398  fourierdlem81  47400  fourierdlem82  47401  fourierdlem93  47412  fourierdlem103  47422  fourierdlem104  47423  sqwvfoura  47441  fourierswlem  47443  elaa2lem  47446  elaa2  47447  etransclem4  47451  etransclem24  47471  etransclem31  47478  etransclem32  47479  etransclem35  47482  sge0repnf  47599  sge0fodjrnlem  47629  sge0iunmpt  47631  sge0rpcpnf  47634  nnfoctbdjlem  47668  meadjun  47675  voliunsge0lem  47685  hoicvr  47761  ovnn0val  47764  ovnsubaddlem1  47783  hoidmvn0val  47797  hsphoidmvle  47799  hoidmv1lelem1  47804  hoidmv1lelem2  47805  hoidmv1lelem3  47806  ovnhoilem1  47814  ovnsubadd2lem  47858  ovnovollem3  47871  cjnpoly  48142  lighneallem3  48895  divgcdoddALTV  48983  isubgr0uhgr  49174  usgrexmpl2trifr  49338  gpg5nbgrvtx03star  49381  gpg5nbgr3star  49382  smprngprmrng  49639  dignn0flhalflem1  49930  itcoval2  49979  itcoval3  49980  itcovalsuc  49982  ackvalsuc1mpt  49993  line2xlem  50068  nellindf  51248  veronesev1lem  51251  veronesev2lem  51252  veronesev3lem  51253  veronesev4lem  51254  veronesev5lem  51255  veronesev6lem  51256  veronesevrowd  51257