Theorem neneqd 2969

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1567   ≠ wne 2964

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 210  df-ne 2965

This theorem is referenced by:  neneq  2970  necon2bi  2994  necon2i  2998  necon4i  2999  pm2.21ddne  3048  mteqand  3055  nelrdva  3677  eldifsnneq  4763  disjprg  5109  0inp0  5332  nelrnmpt  5960  rnmptn0  6248  resf1extb  7933  frxp2  8142  frxp3  8149  onnseq  8333  finnzfsuppd  9335  sniffsupp  9362  scotteld  9874  dfac2b  10116  ackbij1lem15  10218  ttukeylem7  10501  fpwwe2lem12  10629  canthnumlem  10635  canthp1lem2  10640  recgt0  12063  nnneneg  12273  elnnz  12603  xrnemnf  13144  xrnepnf  13145  fzprval  13615  fzodisjsn  13728  fzone1  13815  expnnval  14102  znsqcld  14200  hashelne0d  14406  elprchashprn2  14434  hashpss  14448  relexpsucnnr  15064  relexp1g  15065  relexpuzrel  15091  sgnp  15129  sgn0bi  15142  sgnmul  15146  fprodn0f  16047  ruclem12  16299  dvdsle  16370  nndvdslegcd  16565  gcdnncl  16567  divgcdnn  16575  nn0rppwr  16621  sqgcd  16622  eucalgf  16643  eucalginv  16644  lcmgcdlem  16666  lcmftp  16696  lcmfunsnlem2lem1  16698  lcmfunsnlem2lem2  16699  qredeu  16718  rpdvds  16720  cncongr2  16728  divnumden  16809  divdenle  16810  phisum  16852  oddprm  16872  pythagtriplem4  16881  pythagtriplem8  16885  pythagtriplem9  16886  4sqlem10  17009  ram0  17084  cat1lem  18155  isipodrs  18595  chnub  18680  chnpof1  18688  gsumval2  18746  smndex1n0mnd  18976  smndex2dnrinv  18979  mulgnn  19143  sylow1lem1  19670  gsumval3eu  19976  ablsimpgfindlem1  20181  ablsimpgfindlem2  20182  ablsimpgfind  20184  fincygsubgodd  20186  submomnd  20204  rrgnz  20791  fidomndrng  20857  abvtrivd  20915  ornglmullt  20952  orngrmullt  20953  suborng  20959  00lss  21042  lvecvscan2  21216  0ringprmidl  21448  qsidomlem1  21451  ssdifidlprm  21457  prmirredlem  21593  ofldchr  21697  uvcff  21912  mvrcl  22112  mplmon  22157  mplmonmul  22158  psdmul  22300  coe1tmfv2  22407  cply1coe0  22432  cply1coe0bi  22433  1marepvsma1  22711  mdetrsca2  22732  mdetrlin2  22735  mdetunilem2  22741  mdetunilem5  22744  mdetunilem6  22745  mdetunilem9  22748  maducoeval2  22768  gsummatr01lem3  22785  gsummatr01lem4  22786  gsummatr01  22787  m2cpm  22869  m2cpminvid2lem  22882  fvmptnn04ifa  22978  fvmptnn04ifb  22979  fvmptnn04ifc  22980  chfacffsupp  22984  chfacfscmul0  22986  chfacfscmulgsum  22988  chfacfpmmul0  22990  chfacfpmmulgsum  22992  connclo  23543  dissnlocfin  23657  ptpjpre2  23708  txindis  23762  snfil  23992  alexsublem  24172  tsmsfbas  24256  stdbdxmet  24643  dscmet  24700  xrsxmet  24938  iccpnfcnv  25074  cphsubrglem  25307  minveclem3b  25558  minveclem4a  25560  ovolicc1  25646  dvexp2  26084  dvmptdiv  26104  lhop2  26145  deg1sublt  26238  ig1pval3  26306  dvply1  26416  plydiveu  26430  quotcan  26441  aaliou3lem9  26482  taylthlem2  26505  pserdvlem2  26559  abelthlem9  26571  logccne0  26711  logtayllem  26792  logtayl  26793  cxpef  26798  rtprmirr  26893  angrtmuld  26941  isosctrlem3  26953  chordthmlem  26965  leibpilem2  27074  leibpi  27075  rlimcnp2  27099  efrlim  27102  vma1  27298  muinv  27325  lgsval2lem  27439  lgsval4  27449  lgsdir  27464  lgseisenlem4  27510  lgsquadlem1  27512  lgsquad2  27518  m1lgs  27520  2sqlem8a  27557  2sqlem8  27558  2sqcoprm  27567  2sqmod  27568  padicabv  27762  ostth1  27765  ostth3  27770  nolesgn2ores  27804  nogesgn1ores  27806  nosep1o  27813  nosep2o  27814  nosepdmlem  27815  nosepssdm  27818  noresle  27829  nosupbnd1lem3  27842  nosupbnd1lem4  27843  nosupbnd1lem5  27844  nosupbnd1lem6  27845  nosupbnd2lem1  27847  noinfbnd1lem3  27857  noinfbnd1lem4  27858  noinfbnd1lem5  27859  noinfbnd1lem6  27860  noinfbnd2lem1  27862  0elold  28071  elnnzs  28562  expnnsval  28587  expsne0  28597  bdayfinbndlem1  28628  tgbtwnne  28727  tgbtwndiff  28743  tgcolg  28791  tgbtwnconn1lem3  28811  legso  28836  tglineeltr  28868  tglineintmo  28879  tglineneq  28882  colline  28887  tglnpt4  28892  mirne  28908  miriso  28911  mirhl  28920  mirbtwnhl  28921  symquadlem  28930  krippenlem  28931  midexlem  28933  ragncol  28950  footexALT  28959  footexlem2  28961  colperp  28971  colperpexlem3  28974  mideulem2  28976  opphllem  28977  midex  28979  opptgdim2  28987  oppperpex  28995  hlpasch  28999  colopp  29012  lnincplng  29026  plngrotlem1  29029  plngrotlem2  29030  lnssplnglem  29033  lnssplng  29034  lmieu  29053  trgcopy  29074  cgracol  29098  cgrg3col4  29127  prlngin0  29151  prlngpln  29152  prlnghpg  29153  prlngex  29156  prlngmolem1  29157  prlngmolem2  29158  axlowdimlem15  29249  axcontlem2  29258  axcontlem7  29263  1egrvtxdg0  29804  2pthnloop  30023  cyclnspth  30093  eupth2lem1  30512  eupth2lem2  30513  eupth2lem3lem6  30527  nrt2irr  30767  strlem6  32551  hstrlem6  32559  atssma  32673  chirredlem1  32685  snsssng  32803  ifnetrue  32836  ifnefals  32837  fmptunsnop  32988  xaddeq0  33041  rexmul2  33042  xlt2addrd  33047  xnn0nn0d  33060  elq2  33099  divnumden2  33103  2exple2exp  33121  pmtridf1o  33357  pmtridfv1  33358  pmtridfv2  33359  elrgspnlem2  33506  elrgspnlem3  33507  domnprodeq0  33542  fracfld  33574  pidlnz  33635  lindssn  33637  drngidl  33687  drngidlhash  33688  mxidlmaxv  33698  mxidlprm  33700  mxidlirredi  33701  mxidlirred  33702  krull  33708  drnglring  33729  dflring3  33734  dflring4  33735  rsprprmprmidlb  33760  rprmasso2  33763  pidufd  33780  1arithufdlem3  33783  dfufd2  33787  zringidom  33788  0ringmon1p  33794  ig1pnunit  33838  mplmulmvr  33876  psrmonmul  33887  esplyfval2  33902  esplymhp  33905  esplyfval3  33909  vietadeg1  33915  lindsunlem  33961  fldextrspundgdvdslem  34017  fldext2rspun  34019  ply1annnr  34040  fldext2chn  34065  constrextdg2lem  34085  constrext2chnlem  34087  constrcon  34111  2sqr3minply  34117  cos9thpiminply  34125  1smat1  34141  submatminr1  34147  madjusmdetlem2  34165  zarcls1  34206  zarclsint  34209  zarclssn  34210  xrge0iifcnv  34270  xrge0iifcv  34271  xrge0iif1  34275  qqhval2lem  34318  qqhf  34323  qqhre  34357  esumrnmpt2  34405  esumcvgre  34428  inelpisys  34491  carsgclctunlem2  34656  ballotlemirc  34869  signswlid  34893  repr0  34945  reprlt  34953  reprgt  34955  reprinfz1  34956  tgoldbachgtda  34995  tgoldbachgt  34997  bnj1523  35406  kard0b  35507  acycgr2v  35577  fmlaomn0  35817  fmlasucdisj  35826  fz0n  36158  dfrdg2  36220  dfrdg4  36378  broutsideof2  36549  outsidele  36559  rankeq1o  36598  ivthALT  36771  limsucncmpi  36881  mh-inf3sn  36978  qdiff  37896  topdifinffinlem  37918  icorempo  37922  finxpreclem2  37961  finxp1o  37963  finxpreclem6  37967  poimirlem9  38205  poimirlem11  38207  poimirlem12  38208  poimirlem25  38221  fdc  38321  heibor1lem  38385  heiborlem4  38390  heiborlem6  38392  disjressuc2  38987  2atm  40228  lhpocnle  40717  lhp2at0nle  40736  trlval3  40888  cdleme18c  40994  cdlemg17b  41363  cdlemg17i  41370  dia2dimlem2  41766  dia2dimlem3  41767  dihord6apre  41957  dihatlat  42035  dochshpsat  42155  lcfrlem9  42251  mapdhval2  42427  hdmap1val2  42501  hdmap14lem4a  42572  hdmap14lem6  42574  dvrelogpow2b  42762  aks4d1p1p4  42765  aks4d1p6  42775  fldhmf1  42784  primrootspoweq0  42800  aks6d1c2p2  42813  hashscontpow  42816  aks6d1c5  42833  sticksstones1  42840  sticksstones10  42849  sticksstones12a  42851  sticksstones12  42852  sticksstones22  42862  aks6d1c6lem4  42867  aks6d1c7lem1  42874  aks6d1c7  42878  aks5lem8  42895  quadfac  42899  negn0nposznnd  42970  mhpind  43255  prjspner1  43287  dffltz  43295  3cubeslem2  43345  jm2.26lem3  43657  kelac1  43719  cantnfresb  43980  tfsconcat0b  44002  nlimsuc  44096  clsk1indlem0  44696  sineq0ALT  45574  refsum2cnlem1  45686  disjxp1  45718  disjf1  45830  disjrnmpt2  45835  disjinfi  45839  oddfl  45926  xrlttri5d  45932  supxrge  45983  nepnfltpnf  45987  nemnftgtmnft  45989  xrlexaddrp  45997  xrred  46009  supminfxr2  46112  icoiccdif  46169  qinioo  46180  ioonct  46182  fmul01lt1lem1  46229  climrec  46248  limcperiod  46273  reclimc  46296  limsupub  46347  liminflbuz2  46458  cncfiooicclem1  46536  cncfioobdlem  46539  fperdvper  46562  dvdivbd  46566  ditgeqiooicc  46603  itgsincmulx  46617  itgioocnicc  46620  iblcncfioo  46621  stoweidlem35  46678  stoweidlem39  46682  stirlinglem5  46721  stirlinglem8  46724  dirkerper  46739  dirkercncflem2  46747  dirkercncflem4  46749  fourierdlem31  46781  fourierdlem34  46784  fourierdlem41  46791  fourierdlem42  46792  fourierdlem44  46794  fourierdlem48  46797  fourierdlem49  46798  fourierdlem53  46802  fourierdlem56  46805  fourierdlem58  46807  fourierdlem60  46809  fourierdlem61  46810  fourierdlem62  46811  fourierdlem65  46814  fourierdlem66  46815  fourierdlem73  46822  fourierdlem76  46825  fourierdlem79  46828  fourierdlem81  46830  fourierdlem82  46831  fourierdlem93  46842  fourierdlem103  46852  fourierdlem104  46853  sqwvfoura  46871  fourierswlem  46873  elaa2lem  46876  elaa2  46877  etransclem4  46881  etransclem24  46901  etransclem31  46908  etransclem32  46909  etransclem35  46912  sge0repnf  47029  sge0fodjrnlem  47059  sge0iunmpt  47061  sge0rpcpnf  47064  nnfoctbdjlem  47098  meadjun  47105  voliunsge0lem  47115  hoicvr  47191  ovnn0val  47194  ovnsubaddlem1  47213  hoidmvn0val  47227  hsphoidmvle  47229  hoidmv1lelem1  47234  hoidmv1lelem2  47235  hoidmv1lelem3  47236  ovnhoilem1  47244  ovnsubadd2lem  47288  ovnovollem3  47301  cjnpoly  47552  lighneallem3  48285  divgcdoddALTV  48373  isubgr0uhgr  48564  usgrexmpl2trifr  48728  gpg5nbgrvtx03star  48771  gpg5nbgr3star  48772  smprngprmrng  49030  dignn0flhalflem1  49317  itcoval2  49366  itcoval3  49367  itcovalsuc  49369  ackvalsuc1mpt  49380  line2xlem  49455