Theorem neneqd 2938

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1542   ≠ wne 2933

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 207  df-ne 2934

This theorem is referenced by:  neneq  2939  necon2bi  2963  necon2i  2967  necon4i  2968  pm2.21ddne  3017  mteqand  3024  nelrdva  3652  eldifsnneq  4735  disjprg  5082  0inp0  5296  nelrnmpt  5916  rnmptn0  6202  resf1extb  7878  frxp2  8087  frxp3  8094  onnseq  8277  finnzfsuppd  9279  sniffsupp  9306  dfac2b  10044  ackbij1lem15  10146  ttukeylem7  10428  fpwwe2lem12  10556  canthnumlem  10562  canthp1lem2  10567  recgt0  11992  nnneneg  12203  elnnz  12525  xrnemnf  13059  xrnepnf  13060  fzprval  13530  fzodisjsn  13643  fzone1  13730  expnnval  14017  znsqcld  14115  hashelne0d  14321  elprchashprn2  14349  relexpsucnnr  14978  relexp1g  14979  relexpuzrel  15005  sgnp  15043  fprodn0f  15947  ruclem12  16199  dvdsle  16270  nndvdslegcd  16465  gcdnncl  16467  divgcdnn  16475  nn0rppwr  16521  sqgcd  16522  eucalgf  16543  eucalginv  16544  lcmgcdlem  16566  lcmftp  16596  lcmfunsnlem2lem1  16598  lcmfunsnlem2lem2  16599  qredeu  16618  rpdvds  16620  cncongr2  16628  divnumden  16709  divdenle  16710  phisum  16752  oddprm  16772  pythagtriplem4  16781  pythagtriplem8  16785  pythagtriplem9  16786  4sqlem10  16909  ram0  16984  cat1lem  18054  isipodrs  18494  chnub  18579  chnpof1  18587  gsumval2  18645  smndex1n0mnd  18874  smndex2dnrinv  18877  mulgnn  19042  sylow1lem1  19564  gsumval3eu  19870  ablsimpgfindlem1  20075  ablsimpgfindlem2  20076  ablsimpgfind  20078  fincygsubgodd  20080  submomnd  20098  rrgnz  20672  fidomndrng  20741  abvtrivd  20800  ornglmullt  20837  orngrmullt  20838  suborng  20844  00lss  20927  lvecvscan2  21102  prmirredlem  21462  ofldchr  21566  uvcff  21781  mvrcl  21980  mplmon  22023  mplmonmul  22024  psdmul  22142  coe1tmfv2  22250  cply1coe0  22276  cply1coe0bi  22277  1marepvsma1  22558  mdetrsca2  22579  mdetrlin2  22582  mdetunilem2  22588  mdetunilem5  22591  mdetunilem6  22592  mdetunilem9  22595  maducoeval2  22615  gsummatr01lem3  22632  gsummatr01lem4  22633  gsummatr01  22634  m2cpm  22716  m2cpminvid2lem  22729  fvmptnn04ifa  22825  fvmptnn04ifb  22826  fvmptnn04ifc  22827  chfacffsupp  22831  chfacfscmul0  22833  chfacfscmulgsum  22835  chfacfpmmul0  22837  chfacfpmmulgsum  22839  connclo  23390  dissnlocfin  23504  ptpjpre2  23555  txindis  23609  snfil  23839  alexsublem  24019  tsmsfbas  24103  stdbdxmet  24490  dscmet  24547  xrsxmet  24785  iccpnfcnv  24921  cphsubrglem  25154  minveclem3b  25405  minveclem4a  25407  ovolicc1  25493  dvexp2  25931  dvmptdiv  25951  lhop2  25992  deg1sublt  26085  ig1pval3  26153  dvply1  26260  plydiveu  26275  quotcan  26286  aaliou3lem9  26327  taylthlem2  26351  taylthlem2OLD  26352  pserdvlem2  26406  abelthlem9  26418  logccne0  26555  logtayllem  26636  logtayl  26637  cxpef  26642  rtprmirr  26737  angrtmuld  26785  isosctrlem3  26797  chordthmlem  26809  leibpilem2  26918  leibpi  26919  rlimcnp2  26943  efrlim  26946  efrlimOLD  26947  vma1  27143  muinv  27170  lgsval2lem  27284  lgsval4  27294  lgsdir  27309  lgseisenlem4  27355  lgsquadlem1  27357  lgsquad2  27363  m1lgs  27365  2sqlem8a  27402  2sqlem8  27403  2sqcoprm  27412  2sqmod  27413  padicabv  27607  ostth1  27610  ostth3  27615  nolesgn2ores  27650  nogesgn1ores  27652  nosep1o  27659  nosep2o  27660  nosepdmlem  27661  nosepssdm  27664  noresle  27675  nosupbnd1lem3  27688  nosupbnd1lem4  27689  nosupbnd1lem5  27690  nosupbnd1lem6  27691  nosupbnd2lem1  27693  noinfbnd1lem3  27703  noinfbnd1lem4  27704  noinfbnd1lem5  27705  noinfbnd1lem6  27706  noinfbnd2lem1  27708  0elold  27916  elnnzs  28407  expnnsval  28432  expsne0  28442  bdayfinbndlem1  28473  tgbtwnne  28572  tgbtwndiff  28588  tgcolg  28636  tgbtwnconn1lem3  28656  legso  28681  tglineeltr  28713  tglineintmo  28724  tglineneq  28726  colline  28731  mirne  28749  miriso  28752  mirhl  28761  mirbtwnhl  28762  symquadlem  28771  krippenlem  28772  midexlem  28774  ragncol  28791  footexALT  28800  footexlem2  28802  colperp  28811  colperpexlem3  28814  mideulem2  28816  opphllem  28817  midex  28819  opptgdim2  28827  oppperpex  28835  hlpasch  28838  colopp  28851  lmieu  28866  trgcopy  28886  cgracol  28910  cgrg3col4  28935  axlowdimlem15  29039  axcontlem2  29048  axcontlem7  29053  1egrvtxdg0  29595  2pthnloop  29814  cyclnspth  29884  eupth2lem1  30303  eupth2lem2  30304  eupth2lem3lem6  30318  nrt2irr  30558  strlem6  32342  hstrlem6  32350  atssma  32464  chirredlem1  32476  snsssng  32599  ifnetrue  32632  ifnefals  32633  fmptunsnop  32788  xaddeq0  32841  rexmul2  32842  xlt2addrd  32847  xnn0nn0d  32860  hashpss  32897  elq2  32900  divnumden2  32904  sgnmul  32923  sgn0bi  32928  2exple2exp  32933  pmtridf1o  33170  pmtridfv1  33171  pmtridfv2  33172  elrgspnlem2  33319  elrgspnlem3  33320  domnprodeq0  33352  fracfld  33384  pidlnz  33451  lindssn  33453  drngidl  33508  drngidlhash  33509  0ringprmidl  33524  qsidomlem1  33527  ssdifidlprm  33533  mxidlmaxv  33543  mxidlprm  33545  mxidlirredi  33546  mxidlirred  33547  krull  33554  rsprprmprmidlb  33598  rprmasso2  33601  pidufd  33618  1arithufdlem3  33621  dfufd2  33625  zringidom  33626  0ringmon1p  33632  ig1pnunit  33676  mplmulmvr  33698  psrmonmul  33709  esplyfval2  33724  esplymhp  33727  esplyfval3  33731  vietadeg1  33737  lindsunlem  33784  fldextrspundgdvdslem  33840  fldext2rspun  33842  ply1annnr  33863  fldext2chn  33888  constrextdg2lem  33908  constrext2chnlem  33910  constrcon  33934  2sqr3minply  33940  cos9thpiminply  33948  1smat1  33964  submatminr1  33970  madjusmdetlem2  33988  zarcls1  34029  zarclsint  34032  zarclssn  34033  xrge0iifcnv  34093  xrge0iifcv  34094  xrge0iif1  34098  qqhval2lem  34141  qqhf  34146  qqhre  34180  esumrnmpt2  34228  esumcvgre  34251  inelpisys  34314  carsgclctunlem2  34479  ballotlemirc  34692  signswlid  34719  repr0  34771  reprlt  34779  reprgt  34781  reprinfz1  34782  tgoldbachgtda  34821  tgoldbachgt  34823  bnj1523  35229  acycgr2v  35348  fmlaomn0  35588  fmlasucdisj  35597  fz0n  35929  dfrdg2  35991  dfrdg4  36149  broutsideof2  36320  outsidele  36330  rankeq1o  36369  ivthALT  36533  limsucncmpi  36643  mh-inf3sn  36740  topdifinffinlem  37677  icorempo  37681  finxpreclem2  37720  finxp1o  37722  finxpreclem6  37726  poimirlem9  37964  poimirlem11  37966  poimirlem12  37967  poimirlem25  37980  fdc  38080  heibor1lem  38144  heiborlem4  38149  heiborlem6  38151  disjressuc2  38746  2atm  39987  lhpocnle  40476  lhp2at0nle  40495  trlval3  40647  cdleme18c  40753  cdlemg17b  41122  cdlemg17i  41129  dia2dimlem2  41525  dia2dimlem3  41526  dihord6apre  41716  dihatlat  41794  dochshpsat  41914  lcfrlem9  42010  mapdhval2  42186  hdmap1val2  42260  hdmap14lem4a  42331  hdmap14lem6  42333  dvrelogpow2b  42521  aks4d1p1p4  42524  aks4d1p6  42534  fldhmf1  42543  primrootspoweq0  42559  aks6d1c2p2  42572  hashscontpow  42575  aks6d1c5  42592  sticksstones1  42599  sticksstones10  42608  sticksstones12a  42610  sticksstones12  42611  sticksstones22  42621  aks6d1c6lem4  42626  aks6d1c7lem1  42633  aks6d1c7  42637  aks5lem8  42654  negn0nposznnd  42728  mhpind  43041  prjspner1  43073  dffltz  43081  3cubeslem2  43131  jm2.26lem3  43447  kelac1  43509  cantnfresb  43770  tfsconcat0b  43792  nlimsuc  43886  clsk1indlem0  44486  scotteld  44691  sineq0ALT  45381  refsum2cnlem1  45486  disjxp1  45518  disjf1  45631  disjrnmpt2  45636  disjinfi  45640  oddfl  45729  xrlttri5d  45735  supxrge  45786  nepnfltpnf  45790  nemnftgtmnft  45792  xrlexaddrp  45800  xrred  45812  supminfxr2  45915  icoiccdif  45972  qinioo  45983  ioonct  45985  fmul01lt1lem1  46032  climrec  46051  limcperiod  46076  reclimc  46099  limsupub  46150  liminflbuz2  46261  cncfiooicclem1  46339  cncfioobdlem  46342  fperdvper  46365  dvdivbd  46369  ditgeqiooicc  46406  itgsincmulx  46420  itgioocnicc  46423  iblcncfioo  46424  stoweidlem35  46481  stoweidlem39  46485  stirlinglem5  46524  stirlinglem8  46527  dirkerper  46542  dirkercncflem2  46550  dirkercncflem4  46552  fourierdlem31  46584  fourierdlem34  46587  fourierdlem41  46594  fourierdlem42  46595  fourierdlem44  46597  fourierdlem48  46600  fourierdlem49  46601  fourierdlem53  46605  fourierdlem56  46608  fourierdlem58  46610  fourierdlem60  46612  fourierdlem61  46613  fourierdlem62  46614  fourierdlem65  46617  fourierdlem66  46618  fourierdlem73  46625  fourierdlem76  46628  fourierdlem79  46631  fourierdlem81  46633  fourierdlem82  46634  fourierdlem93  46645  fourierdlem103  46655  fourierdlem104  46656  sqwvfoura  46674  fourierswlem  46676  elaa2lem  46679  elaa2  46680  etransclem4  46684  etransclem24  46704  etransclem31  46711  etransclem32  46712  etransclem35  46715  sge0repnf  46832  sge0fodjrnlem  46862  sge0iunmpt  46864  sge0rpcpnf  46867  nnfoctbdjlem  46901  meadjun  46908  voliunsge0lem  46918  hoicvr  46994  ovnn0val  46997  ovnsubaddlem1  47016  hoidmvn0val  47030  hsphoidmvle  47032  hoidmv1lelem1  47037  hoidmv1lelem2  47038  hoidmv1lelem3  47039  ovnhoilem1  47047  ovnsubadd2lem  47091  ovnovollem3  47104  cjnpoly  47349  lighneallem3  48082  divgcdoddALTV  48170  isubgr0uhgr  48361  usgrexmpl2trifr  48525  gpg5nbgrvtx03star  48568  gpg5nbgr3star  48569  dignn0flhalflem1  49103  itcoval2  49152  itcoval3  49153  itcovalsuc  49155  ackvalsuc1mpt  49166  line2xlem  49241