Theorem neneqd 2992

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1538   ≠ wne 2987

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 2988

This theorem is referenced by:  neneq  2993  necon2bi  3017  necon2i  3021  necon4i  3022  pm2.21ddne  3071  mteqand  3090  nelrdva  3644  eldifsnneq  4684  disjprg  5026  0inp0  5224  onnseq  7964  sniffsupp  8857  dfac2b  9541  ackbij1lem15  9645  ttukeylem7  9926  fpwwe2lem13  10053  canthnumlem  10059  canthp1lem2  10064  recgt0  11475  nnneneg  11660  elnnz  11979  xrnemnf  12500  xrnepnf  12501  fzprval  12963  fzodisjsn  13070  expnnval  13428  znsqcld  13522  hashelne0d  13725  elprchashprn2  13753  relexpsucnnr  14376  relexp1g  14377  relexpuzrel  14403  sgnp  14441  fprodn0f  15337  ruclem12  15586  dvdsle  15652  nndvdslegcd  15844  gcdnncl  15846  divgcdnn  15853  sqgcd  15899  eucalgf  15917  eucalginv  15918  lcmgcdlem  15940  lcmftp  15970  lcmfunsnlem2lem1  15972  lcmfunsnlem2lem2  15973  qredeu  15992  rpdvds  15994  cncongr2  16002  divnumden  16078  divdenle  16079  phisum  16117  oddprm  16137  pythagtriplem4  16146  pythagtriplem8  16150  pythagtriplem9  16151  4sqlem10  16273  ram0  16348  isipodrs  17763  gsumval2  17888  smndex1n0mnd  18069  smndex2dnrinv  18072  mulgnn  18224  sylow1lem1  18715  gsumval3eu  19017  ablsimpgfindlem1  19222  ablsimpgfindlem2  19223  ablsimpgfind  19225  fincygsubgodd  19227  abvtrivd  19604  00lss  19706  lvecvscan2  19877  fidomndrng  20073  prmirredlem  20186  uvcff  20480  mvrcl  20688  mplmon  20703  mplmonmul  20704  coe1tmfv2  20904  cply1coe0  20928  cply1coe0bi  20929  1marepvsma1  21188  mdetrsca2  21209  mdetrlin2  21212  mdetunilem2  21218  mdetunilem5  21221  mdetunilem6  21222  mdetunilem9  21225  maducoeval2  21245  gsummatr01lem3  21262  gsummatr01lem4  21263  gsummatr01  21264  m2cpm  21346  m2cpminvid2lem  21359  fvmptnn04ifa  21455  fvmptnn04ifb  21456  fvmptnn04ifc  21457  chfacffsupp  21461  chfacfscmul0  21463  chfacfscmulgsum  21465  chfacfpmmul0  21467  chfacfpmmulgsum  21469  connclo  22020  dissnlocfin  22134  ptpjpre2  22185  txindis  22239  snfil  22469  alexsublem  22649  tsmsfbas  22733  stdbdxmet  23122  dscmet  23179  xrsxmet  23414  iccpnfcnv  23549  cphsubrglem  23782  minveclem3b  24032  minveclem4a  24034  ovolicc1  24120  dvexp2  24557  dvmptdiv  24577  lhop2  24618  deg1sublt  24711  ig1pval3  24775  dvply1  24880  plydiveu  24894  quotcan  24905  aaliou3lem9  24946  taylthlem2  24969  pserdvlem2  25023  abelthlem9  25035  logccne0  25170  logtayllem  25250  logtayl  25251  cxpef  25256  angrtmuld  25394  isosctrlem3  25406  chordthmlem  25418  leibpilem2  25527  leibpi  25528  rlimcnp2  25552  efrlim  25555  vma1  25751  muinv  25778  lgsval2lem  25891  lgsval4  25901  lgsdir  25916  lgseisenlem4  25962  lgsquadlem1  25964  lgsquad2  25970  m1lgs  25972  2sqlem8a  26009  2sqlem8  26010  2sqcoprm  26019  2sqmod  26020  padicabv  26214  ostth1  26217  ostth3  26222  tgbtwnne  26284  tgbtwndiff  26300  tgcolg  26348  tgbtwnconn1lem3  26368  legso  26393  tglineeltr  26425  tglineintmo  26436  tglineneq  26438  colline  26443  mirne  26461  miriso  26464  mirhl  26473  mirbtwnhl  26474  symquadlem  26483  krippenlem  26484  midexlem  26486  ragncol  26503  footexALT  26512  footexlem2  26514  colperp  26523  colperpexlem3  26526  mideulem2  26528  opphllem  26529  midex  26531  opptgdim2  26539  oppperpex  26547  hlpasch  26550  colopp  26563  lmieu  26578  trgcopy  26598  cgracol  26622  cgrg3col4  26647  axlowdimlem15  26750  axcontlem2  26759  axcontlem7  26764  1egrvtxdg0  27301  2pthnloop  27520  cyclnspth  27589  eupth2lem1  28003  eupth2lem2  28004  eupth2lem3lem6  28018  strlem6  30039  hstrlem6  30047  atssma  30161  chirredlem1  30173  snsssng  30284  xaddeq0  30503  xlt2addrd  30508  fzone1  30549  divnumden2  30560  submomnd  30761  pmtridf1o  30786  pmtridfv1  30787  pmtridfv2  30788  ornglmullt  30931  orngrmullt  30932  ofldchr  30938  suborng  30939  pidlnz  30991  lindssn  30993  0ringprmidl  31033  qsidomlem1  31036  mxidlprm  31048  krull  31051  lindsunlem  31108  1smat1  31157  submatminr1  31163  madjusmdetlem2  31181  zarcls1  31222  zarclsint  31225  zarclssn  31226  xrge0iifcnv  31286  xrge0iifcv  31287  xrge0iif1  31291  qqhval2lem  31332  qqhf  31337  qqhre  31371  esumrnmpt2  31437  esumcvgre  31460  inelpisys  31523  carsgclctunlem2  31687  ballotlemirc  31899  sgnmul  31910  sgn0bi  31915  signswlid  31939  repr0  31992  reprlt  32000  reprgt  32002  reprinfz1  32003  tgoldbachgtda  32042  tgoldbachgt  32044  bnj1523  32453  acycgr2v  32510  fmlaomn0  32750  fmlasucdisj  32759  fz0n  33075  dfrdg2  33153  nolesgn2ores  33292  nosep1o  33299  nosepdmlem  33300  nosepssdm  33303  noresle  33313  nosupbnd1lem3  33323  nosupbnd1lem4  33324  nosupbnd1lem5  33325  nosupbnd1lem6  33326  nosupbnd2lem1  33328  dfrdg4  33525  broutsideof2  33696  outsidele  33706  rankeq1o  33745  ivthALT  33796  limsucncmpi  33906  topdifinffinlem  34764  icorempo  34768  finxpreclem2  34807  finxp1o  34809  finxpreclem6  34813  poimirlem9  35066  poimirlem11  35068  poimirlem12  35069  poimirlem25  35082  fdc  35183  heibor1lem  35247  heiborlem4  35252  heiborlem6  35254  2atm  36823  lhpocnle  37312  lhp2at0nle  37331  trlval3  37483  cdleme18c  37589  cdlemg17b  37958  cdlemg17i  37965  dia2dimlem2  38361  dia2dimlem3  38362  dihord6apre  38552  dihatlat  38630  dochshpsat  38750  lcfrlem9  38846  mapdhval2  39022  hdmap1val2  39096  hdmap14lem4a  39167  hdmap14lem6  39169  metakunt6  39355  metakunt7  39356  metakunt11  39360  metakunt12  39361  metakunt27  39376  metakunt28  39377  metakunt29  39378  metakunt30  39379  negn0nposznnd  39476  nn0rppwr  39490  rtprmirr  39502  dffltz  39615  3cubeslem2  39626  jm2.26lem3  39942  kelac1  40007  clsk1indlem0  40744  finnzfsuppd  40915  scotteld  40954  sineq0ALT  41643  refsum2cnlem1  41666  disjxp1  41703  nelrnmpt  41720  disjf1  41809  disjrnmpt2  41815  disjinfi  41820  rnmptn0  41850  oddfl  41908  xrlttri5d  41914  supxrge  41970  nepnfltpnf  41974  nemnftgtmnft  41976  xrlexaddrp  41984  xrred  41997  supminfxr2  42108  icoiccdif  42161  qinioo  42172  ioonct  42174  fmul01lt1lem1  42226  climrec  42245  limcperiod  42270  reclimc  42295  limsupub  42346  liminflbuz2  42457  cncfiooicclem1  42535  cncfioobdlem  42538  fperdvper  42561  dvdivbd  42565  ditgeqiooicc  42602  itgsincmulx  42616  itgioocnicc  42619  iblcncfioo  42620  stoweidlem35  42677  stoweidlem39  42681  stirlinglem5  42720  stirlinglem8  42723  dirkerper  42738  dirkercncflem2  42746  dirkercncflem4  42748  fourierdlem31  42780  fourierdlem34  42783  fourierdlem41  42790  fourierdlem42  42791  fourierdlem44  42793  fourierdlem48  42796  fourierdlem49  42797  fourierdlem53  42801  fourierdlem56  42804  fourierdlem58  42806  fourierdlem60  42808  fourierdlem61  42809  fourierdlem62  42810  fourierdlem65  42813  fourierdlem66  42814  fourierdlem73  42821  fourierdlem76  42824  fourierdlem79  42827  fourierdlem81  42829  fourierdlem82  42830  fourierdlem93  42841  fourierdlem103  42851  fourierdlem104  42852  sqwvfoura  42870  fourierswlem  42872  elaa2lem  42875  elaa2  42876  etransclem4  42880  etransclem24  42900  etransclem31  42907  etransclem32  42908  etransclem35  42911  sge0repnf  43025  sge0fodjrnlem  43055  sge0iunmpt  43057  sge0rpcpnf  43060  nnfoctbdjlem  43094  meadjun  43101  voliunsge0lem  43111  hoicvr  43187  ovnn0val  43190  ovnsubaddlem1  43209  hoidmvn0val  43223  hsphoidmvle  43225  hoidmv1lelem1  43230  hoidmv1lelem2  43231  hoidmv1lelem3  43232  ovnhoilem1  43240  ovnsubadd2lem  43284  ovnovollem3  43297  lighneallem3  44125  divgcdoddALTV  44200  dignn0flhalflem1  45029  itcoval2  45078  itcoval3  45079  itcovalsuc  45081  ackvalsuc1mpt  45092  line2xlem  45167