Theorem neneqd 2936

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1539   ≠ wne 2931

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 2932

This theorem is referenced by:  neneq  2937  necon2bi  2961  necon2i  2965  necon4i  2966  pm2.21ddne  3015  mteqand  3022  nelrdva  3693  eldifsnneq  4771  disjprg  5119  0inp0  5339  rnmptn0  6244  resf1extb  7938  frxp2  8151  frxp3  8158  onnseq  8366  finnzfsuppd  9395  sniffsupp  9422  dfac2b  10153  ackbij1lem15  10255  ttukeylem7  10537  fpwwe2lem12  10664  canthnumlem  10670  canthp1lem2  10675  recgt0  12095  nnneneg  12283  elnnz  12606  xrnemnf  13141  xrnepnf  13142  fzprval  13607  fzodisjsn  13719  expnnval  14087  znsqcld  14185  hashelne0d  14390  elprchashprn2  14418  relexpsucnnr  15047  relexp1g  15048  relexpuzrel  15074  sgnp  15112  fprodn0f  16010  ruclem12  16260  dvdsle  16330  nndvdslegcd  16525  gcdnncl  16527  divgcdnn  16535  nn0rppwr  16581  sqgcd  16582  eucalgf  16603  eucalginv  16604  lcmgcdlem  16626  lcmftp  16656  lcmfunsnlem2lem1  16658  lcmfunsnlem2lem2  16659  qredeu  16678  rpdvds  16680  cncongr2  16688  divnumden  16768  divdenle  16769  phisum  16811  oddprm  16831  pythagtriplem4  16840  pythagtriplem8  16844  pythagtriplem9  16845  4sqlem10  16968  ram0  17043  cat1lem  18113  isipodrs  18552  gsumval2  18669  smndex1n0mnd  18895  smndex2dnrinv  18898  mulgnn  19063  sylow1lem1  19585  gsumval3eu  19891  ablsimpgfindlem1  20096  ablsimpgfindlem2  20097  ablsimpgfind  20099  fincygsubgodd  20101  rrgnz  20673  fidomndrng  20743  abvtrivd  20802  00lss  20908  lvecvscan2  21083  prmirredlem  21446  uvcff  21766  mvrcl  21967  mplmon  22008  mplmonmul  22009  psdmul  22119  coe1tmfv2  22227  cply1coe0  22254  cply1coe0bi  22255  1marepvsma1  22538  mdetrsca2  22559  mdetrlin2  22562  mdetunilem2  22568  mdetunilem5  22571  mdetunilem6  22572  mdetunilem9  22575  maducoeval2  22595  gsummatr01lem3  22612  gsummatr01lem4  22613  gsummatr01  22614  m2cpm  22696  m2cpminvid2lem  22709  fvmptnn04ifa  22805  fvmptnn04ifb  22806  fvmptnn04ifc  22807  chfacffsupp  22811  chfacfscmul0  22813  chfacfscmulgsum  22815  chfacfpmmul0  22817  chfacfpmmulgsum  22819  connclo  23370  dissnlocfin  23484  ptpjpre2  23535  txindis  23589  snfil  23819  alexsublem  23999  tsmsfbas  24083  stdbdxmet  24473  dscmet  24530  xrsxmet  24768  iccpnfcnv  24912  cphsubrglem  25148  minveclem3b  25399  minveclem4a  25401  ovolicc1  25488  dvexp2  25929  dvmptdiv  25949  lhop2  25991  deg1sublt  26086  ig1pval3  26154  dvply1  26262  plydiveu  26277  quotcan  26288  aaliou3lem9  26329  taylthlem2  26353  taylthlem2OLD  26354  pserdvlem2  26409  abelthlem9  26421  logccne0  26557  logtayllem  26638  logtayl  26639  cxpef  26644  rtprmirr  26740  angrtmuld  26788  isosctrlem3  26800  chordthmlem  26812  leibpilem2  26921  leibpi  26922  rlimcnp2  26946  efrlim  26949  efrlimOLD  26950  vma1  27146  muinv  27173  lgsval2lem  27288  lgsval4  27298  lgsdir  27313  lgseisenlem4  27359  lgsquadlem1  27361  lgsquad2  27367  m1lgs  27369  2sqlem8a  27406  2sqlem8  27407  2sqcoprm  27416  2sqmod  27417  padicabv  27611  ostth1  27614  ostth3  27619  nolesgn2ores  27654  nogesgn1ores  27656  nosep1o  27663  nosep2o  27664  nosepdmlem  27665  nosepssdm  27668  noresle  27679  nosupbnd1lem3  27692  nosupbnd1lem4  27693  nosupbnd1lem5  27694  nosupbnd1lem6  27695  nosupbnd2lem1  27697  noinfbnd1lem3  27707  noinfbnd1lem4  27708  noinfbnd1lem5  27709  noinfbnd1lem6  27710  noinfbnd2lem1  27712  0elold  27884  elnnzs  28324  expsnnval  28346  expsne0  28351  tgbtwnne  28435  tgbtwndiff  28451  tgcolg  28499  tgbtwnconn1lem3  28519  legso  28544  tglineeltr  28576  tglineintmo  28587  tglineneq  28589  colline  28594  mirne  28612  miriso  28615  mirhl  28624  mirbtwnhl  28625  symquadlem  28634  krippenlem  28635  midexlem  28637  ragncol  28654  footexALT  28663  footexlem2  28665  colperp  28674  colperpexlem3  28677  mideulem2  28679  opphllem  28680  midex  28682  opptgdim2  28690  oppperpex  28698  hlpasch  28701  colopp  28714  lmieu  28729  trgcopy  28749  cgracol  28773  cgrg3col4  28798  axlowdimlem15  28902  axcontlem2  28911  axcontlem7  28916  1egrvtxdg0  29458  2pthnloop  29680  cyclnspth  29750  eupth2lem1  30166  eupth2lem2  30167  eupth2lem3lem6  30181  nrt2irr  30421  strlem6  32204  hstrlem6  32212  atssma  32326  chirredlem1  32338  snsssng  32462  ifnetrue  32496  ifnefals  32497  fmptunsnop  32645  xaddeq0  32698  rexmul2  32699  xlt2addrd  32704  xnn0nn0d  32718  fzone1  32746  hashpss  32757  divnumden2  32762  2exple2exp  32779  chnub  32946  submomnd  33031  pmtridf1o  33058  pmtridfv1  33059  pmtridfv2  33060  elrgspnlem2  33191  elrgspnlem3  33192  fracfld  33255  ornglmullt  33282  orngrmullt  33283  ofldchr  33289  suborng  33290  pidlnz  33344  lindssn  33346  drngidl  33401  drngidlhash  33402  0ringprmidl  33417  qsidomlem1  33420  ssdifidlprm  33426  mxidlmaxv  33436  mxidlprm  33438  mxidlirredi  33439  mxidlirred  33440  krull  33447  rsprprmprmidlb  33491  rprmasso2  33494  pidufd  33511  1arithufdlem3  33514  dfufd2  33518  zringidom  33519  0ringmon1p  33523  ig1pnunit  33561  lindsunlem  33615  fldextrspundgdvdslem  33672  fldext2rspun  33674  ply1annnr  33688  fldext2chn  33713  constrextdg2lem  33733  constrext2chnlem  33735  constrcon  33759  2sqr3minply  33765  1smat1  33778  submatminr1  33784  madjusmdetlem2  33802  zarcls1  33843  zarclsint  33846  zarclssn  33847  xrge0iifcnv  33907  xrge0iifcv  33908  xrge0iif1  33912  qqhval2lem  33957  qqhf  33962  qqhre  33996  esumrnmpt2  34044  esumcvgre  34067  inelpisys  34130  carsgclctunlem2  34296  ballotlemirc  34509  sgnmul  34520  sgn0bi  34525  signswlid  34549  repr0  34601  reprlt  34609  reprgt  34611  reprinfz1  34612  tgoldbachgtda  34651  tgoldbachgt  34653  bnj1523  35060  acycgr2v  35130  fmlaomn0  35370  fmlasucdisj  35379  fz0n  35706  dfrdg2  35771  dfrdg4  35927  broutsideof2  36098  outsidele  36108  rankeq1o  36147  ivthALT  36311  limsucncmpi  36421  topdifinffinlem  37323  icorempo  37327  finxpreclem2  37366  finxp1o  37368  finxpreclem6  37372  poimirlem9  37611  poimirlem11  37613  poimirlem12  37614  poimirlem25  37627  fdc  37727  heibor1lem  37791  heiborlem4  37796  heiborlem6  37798  disjressuc2  38364  2atm  39504  lhpocnle  39993  lhp2at0nle  40012  trlval3  40164  cdleme18c  40270  cdlemg17b  40639  cdlemg17i  40646  dia2dimlem2  41042  dia2dimlem3  41043  dihord6apre  41233  dihatlat  41311  dochshpsat  41431  lcfrlem9  41527  mapdhval2  41703  hdmap1val2  41777  hdmap14lem4a  41848  hdmap14lem6  41850  dvrelogpow2b  42044  aks4d1p1p4  42047  aks4d1p6  42057  fldhmf1  42066  primrootspoweq0  42082  aks6d1c2p2  42095  hashscontpow  42098  aks6d1c5  42115  sticksstones1  42122  sticksstones10  42131  sticksstones12a  42133  sticksstones12  42134  sticksstones22  42144  aks6d1c6lem4  42149  aks6d1c7lem1  42156  aks6d1c7  42160  aks5lem8  42177  metakunt6  42186  metakunt7  42187  metakunt11  42191  metakunt12  42192  metakunt27  42207  metakunt28  42208  metakunt29  42209  metakunt30  42210  negn0nposznnd  42296  mhpind  42583  prjspner1  42615  dffltz  42623  3cubeslem2  42674  jm2.26lem3  42991  kelac1  43053  cantnfresb  43314  tfsconcat0b  43336  nlimsuc  43431  clsk1indlem0  44031  scotteld  44237  sineq0ALT  44929  refsum2cnlem1  45014  disjxp1  45046  nelrnmpt  45061  disjf1  45160  disjrnmpt2  45165  disjinfi  45169  oddfl  45261  xrlttri5d  45267  supxrge  45321  nepnfltpnf  45325  nemnftgtmnft  45327  xrlexaddrp  45335  xrred  45348  supminfxr2  45452  icoiccdif  45509  qinioo  45520  ioonct  45522  fmul01lt1lem1  45571  climrec  45590  limcperiod  45615  reclimc  45640  limsupub  45691  liminflbuz2  45802  cncfiooicclem1  45880  cncfioobdlem  45883  fperdvper  45906  dvdivbd  45910  ditgeqiooicc  45947  itgsincmulx  45961  itgioocnicc  45964  iblcncfioo  45965  stoweidlem35  46022  stoweidlem39  46026  stirlinglem5  46065  stirlinglem8  46068  dirkerper  46083  dirkercncflem2  46091  dirkercncflem4  46093  fourierdlem31  46125  fourierdlem34  46128  fourierdlem41  46135  fourierdlem42  46136  fourierdlem44  46138  fourierdlem48  46141  fourierdlem49  46142  fourierdlem53  46146  fourierdlem56  46149  fourierdlem58  46151  fourierdlem60  46153  fourierdlem61  46154  fourierdlem62  46155  fourierdlem65  46158  fourierdlem66  46159  fourierdlem73  46166  fourierdlem76  46169  fourierdlem79  46172  fourierdlem81  46174  fourierdlem82  46175  fourierdlem93  46186  fourierdlem103  46196  fourierdlem104  46197  sqwvfoura  46215  fourierswlem  46217  elaa2lem  46220  elaa2  46221  etransclem4  46225  etransclem24  46245  etransclem31  46252  etransclem32  46253  etransclem35  46256  sge0repnf  46373  sge0fodjrnlem  46403  sge0iunmpt  46405  sge0rpcpnf  46408  nnfoctbdjlem  46442  meadjun  46449  voliunsge0lem  46459  hoicvr  46535  ovnn0val  46538  ovnsubaddlem1  46557  hoidmvn0val  46571  hsphoidmvle  46573  hoidmv1lelem1  46578  hoidmv1lelem2  46579  hoidmv1lelem3  46580  ovnhoilem1  46588  ovnsubadd2lem  46632  ovnovollem3  46645  lighneallem3  47567  divgcdoddALTV  47642  isubgr0uhgr  47832  usgrexmpl2trifr  47969  gpg5nbgrvtx03star  48009  gpg5nbgr3star  48010  dignn0flhalflem1  48509  itcoval2  48558  itcoval3  48559  itcovalsuc  48561  ackvalsuc1mpt  48572  line2xlem  48647