Theorem neneqd 3021

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1537   ≠ wne 3016

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 3017

This theorem is referenced by:  neneq  3022  necon2bi  3046  necon2i  3050  necon4i  3051  pm2.21ddne  3101  mteqand  3122  nelrdva  3696  eldifsnneq  4723  disjprg  5062  0inp0  5259  onnseq  7981  sniffsupp  8873  dfac2b  9556  ackbij1lem15  9656  ttukeylem7  9937  fpwwe2lem13  10064  canthnumlem  10070  canthp1lem2  10075  recgt0  11486  nnneneg  11673  elnnz  11992  xrnemnf  12513  xrnepnf  12514  fzprval  12969  fzodisjsn  13076  expnnval  13433  znsqcld  13527  hashelne0d  13730  elprchashprn2  13758  relexpsucnnr  14384  relexp1g  14385  relexpuzrel  14411  sgnp  14449  fprodn0f  15345  ruclem12  15594  dvdsle  15660  nndvdslegcd  15854  gcdnncl  15856  divgcdnn  15863  sqgcd  15909  eucalgf  15927  eucalginv  15928  lcmgcdlem  15950  lcmftp  15980  lcmfunsnlem2lem1  15982  lcmfunsnlem2lem2  15983  qredeu  16002  rpdvds  16004  cncongr2  16012  divnumden  16088  divdenle  16089  phisum  16127  oddprm  16147  pythagtriplem4  16156  pythagtriplem8  16160  pythagtriplem9  16161  4sqlem10  16283  ram0  16358  isipodrs  17771  gsumval2  17896  smndex1n0mnd  18077  smndex2dnrinv  18080  mulgnn  18232  sylow1lem1  18723  gsumval3eu  19024  ablsimpgfindlem1  19229  ablsimpgfindlem2  19230  ablsimpgfind  19232  fincygsubgodd  19234  abvtrivd  19611  00lss  19713  lvecvscan2  19884  fidomndrng  20080  mvrcl  20229  mplmon  20244  mplmonmul  20245  coe1tmfv2  20443  cply1coe0  20467  cply1coe0bi  20468  prmirredlem  20640  uvcff  20935  1marepvsma1  21192  mdetrsca2  21213  mdetrlin2  21216  mdetunilem2  21222  mdetunilem5  21225  mdetunilem6  21226  mdetunilem9  21229  maducoeval2  21249  gsummatr01lem3  21266  gsummatr01lem4  21267  gsummatr01  21268  m2cpm  21349  m2cpminvid2lem  21362  fvmptnn04ifa  21458  fvmptnn04ifb  21459  fvmptnn04ifc  21460  chfacffsupp  21464  chfacfscmul0  21466  chfacfscmulgsum  21468  chfacfpmmul0  21470  chfacfpmmulgsum  21472  connclo  22023  dissnlocfin  22137  ptpjpre2  22188  txindis  22242  snfil  22472  alexsublem  22652  tsmsfbas  22736  stdbdxmet  23125  dscmet  23182  xrsxmet  23417  iccpnfcnv  23548  cphsubrglem  23781  minveclem3b  24031  minveclem4a  24033  ovolicc1  24117  dvexp2  24551  dvmptdiv  24571  lhop2  24612  deg1sublt  24704  ig1pval3  24768  dvply1  24873  plydiveu  24887  quotcan  24898  aaliou3lem9  24939  taylthlem2  24962  pserdvlem2  25016  abelthlem9  25028  logccne0  25162  logtayllem  25242  logtayl  25243  cxpef  25248  angrtmuld  25386  isosctrlem3  25398  chordthmlem  25410  leibpilem2  25519  leibpi  25520  rlimcnp2  25544  efrlim  25547  vma1  25743  muinv  25770  lgsval2lem  25883  lgsval4  25893  lgsdir  25908  lgseisenlem4  25954  lgsquadlem1  25956  lgsquad2  25962  m1lgs  25964  2sqlem8a  26001  2sqlem8  26002  2sqcoprm  26011  2sqmod  26012  padicabv  26206  ostth1  26209  ostth3  26214  tgbtwnne  26276  tgbtwndiff  26292  tgcolg  26340  tgbtwnconn1lem3  26360  legso  26385  tglineeltr  26417  tglineintmo  26428  tglineneq  26430  colline  26435  mirne  26453  miriso  26456  mirhl  26465  mirbtwnhl  26466  symquadlem  26475  krippenlem  26476  midexlem  26478  ragncol  26495  footexALT  26504  footexlem2  26506  colperp  26515  colperpexlem3  26518  mideulem2  26520  opphllem  26521  midex  26523  opptgdim2  26531  oppperpex  26539  hlpasch  26542  colopp  26555  lmieu  26570  trgcopy  26590  cgracol  26614  cgrg3col4  26639  axlowdimlem15  26742  axcontlem2  26751  axcontlem7  26756  1egrvtxdg0  27293  2pthnloop  27512  cyclnspth  27581  eupth2lem1  27997  eupth2lem2  27998  eupth2lem3lem6  28012  strlem6  30033  hstrlem6  30041  atssma  30155  chirredlem1  30167  xaddeq0  30477  xlt2addrd  30482  fzone1  30523  divnumden2  30534  submomnd  30711  pmtridf1o  30736  pmtridfv1  30737  pmtridfv2  30738  ornglmullt  30880  orngrmullt  30881  ofldchr  30887  suborng  30888  lindssn  30939  qsidomlem1  30965  mxidlprm  30977  krull  30980  lindsunlem  31020  1smat1  31069  submatminr1  31075  madjusmdetlem2  31093  xrge0iifcnv  31176  xrge0iifcv  31177  xrge0iif1  31181  qqhval2lem  31222  qqhf  31227  qqhre  31261  esumrnmpt2  31327  esumcvgre  31350  inelpisys  31413  carsgclctunlem2  31577  ballotlemirc  31789  sgnmul  31800  sgn0bi  31805  signswlid  31829  repr0  31882  reprlt  31890  reprgt  31892  reprinfz1  31893  tgoldbachgtda  31932  tgoldbachgt  31934  bnj1523  32343  acycgr2v  32397  fmlaomn0  32637  fmlasucdisj  32646  fz0n  32962  dfrdg2  33040  nolesgn2ores  33179  nosep1o  33186  nosepdmlem  33187  nosepssdm  33190  noresle  33200  nosupbnd1lem3  33210  nosupbnd1lem4  33211  nosupbnd1lem5  33212  nosupbnd1lem6  33213  nosupbnd2lem1  33215  dfrdg4  33412  broutsideof2  33583  outsidele  33593  rankeq1o  33632  ivthALT  33683  limsucncmpi  33793  topdifinffinlem  34631  icorempo  34635  finxpreclem2  34674  finxp1o  34676  finxpreclem6  34680  poimirlem9  34916  poimirlem11  34918  poimirlem12  34919  poimirlem25  34932  fdc  35035  heibor1lem  35102  heiborlem4  35107  heiborlem6  35109  2atm  36678  lhpocnle  37167  lhp2at0nle  37186  trlval3  37338  cdleme18c  37444  cdlemg17b  37813  cdlemg17i  37820  dia2dimlem2  38216  dia2dimlem3  38217  dihord6apre  38407  dihatlat  38485  dochshpsat  38605  lcfrlem9  38701  mapdhval2  38877  hdmap1val2  38951  hdmap14lem4a  39022  hdmap14lem6  39024  negn0nposznnd  39217  nn0rppwr  39231  rtprmirr  39243  dffltz  39320  3cubeslem2  39331  jm2.26lem3  39647  kelac1  39712  clsk1indlem0  40440  scotteld  40631  sineq0ALT  41320  refsum2cnlem1  41343  disjxp1  41380  nelrnmpt  41397  disjf1  41492  disjrnmpt2  41498  disjinfi  41503  rnmptn0  41533  oddfl  41592  xrlttri5d  41598  supxrge  41655  nepnfltpnf  41659  nemnftgtmnft  41661  xrlexaddrp  41669  xrred  41682  supminfxr2  41794  icoiccdif  41849  qinioo  41860  ioonct  41862  fmul01lt1lem1  41914  climrec  41933  limcperiod  41958  reclimc  41983  limsupub  42034  liminflbuz2  42145  cncfiooicclem1  42225  cncfioobdlem  42228  fperdvper  42252  dvdivbd  42257  ditgeqiooicc  42294  itgsincmulx  42308  itgioocnicc  42311  iblcncfioo  42312  stoweidlem35  42369  stoweidlem39  42373  stirlinglem5  42412  stirlinglem8  42415  dirkerper  42430  dirkercncflem2  42438  dirkercncflem4  42440  fourierdlem31  42472  fourierdlem34  42475  fourierdlem41  42482  fourierdlem42  42483  fourierdlem44  42485  fourierdlem48  42488  fourierdlem49  42489  fourierdlem53  42493  fourierdlem56  42496  fourierdlem58  42498  fourierdlem60  42500  fourierdlem61  42501  fourierdlem62  42502  fourierdlem65  42505  fourierdlem66  42506  fourierdlem73  42513  fourierdlem76  42516  fourierdlem79  42519  fourierdlem81  42521  fourierdlem82  42522  fourierdlem93  42533  fourierdlem103  42543  fourierdlem104  42544  sqwvfoura  42562  fourierswlem  42564  elaa2lem  42567  elaa2  42568  etransclem4  42572  etransclem24  42592  etransclem31  42599  etransclem32  42600  etransclem35  42603  sge0repnf  42717  sge0fodjrnlem  42747  sge0iunmpt  42749  sge0rpcpnf  42752  nnfoctbdjlem  42786  meadjun  42793  voliunsge0lem  42803  hoicvr  42879  ovnn0val  42882  ovnsubaddlem1  42901  hoidmvn0val  42915  hsphoidmvle  42917  hoidmv1lelem1  42922  hoidmv1lelem2  42923  hoidmv1lelem3  42924  ovnhoilem1  42932  ovnsubadd2lem  42976  ovnovollem3  42989  lighneallem3  43821  divgcdoddALTV  43896  dignn0flhalflem1  44724  line2xlem  44789