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  5297  nelrnmpt  5918  rnmptn0  6204  resf1extb  7880  frxp2  8089  frxp3  8096  onnseq  8279  finnzfsuppd  9281  sniffsupp  9308  dfac2b  10048  ackbij1lem15  10150  ttukeylem7  10432  fpwwe2lem12  10560  canthnumlem  10566  canthp1lem2  10571  recgt0  11996  nnneneg  12207  elnnz  12529  xrnemnf  13063  xrnepnf  13064  fzprval  13534  fzodisjsn  13647  fzone1  13734  expnnval  14021  znsqcld  14119  hashelne0d  14325  elprchashprn2  14353  relexpsucnnr  14982  relexp1g  14983  relexpuzrel  15009  sgnp  15047  fprodn0f  15951  ruclem12  16203  dvdsle  16274  nndvdslegcd  16469  gcdnncl  16471  divgcdnn  16479  nn0rppwr  16525  sqgcd  16526  eucalgf  16547  eucalginv  16548  lcmgcdlem  16570  lcmftp  16600  lcmfunsnlem2lem1  16602  lcmfunsnlem2lem2  16603  qredeu  16622  rpdvds  16624  cncongr2  16632  divnumden  16713  divdenle  16714  phisum  16756  oddprm  16776  pythagtriplem4  16785  pythagtriplem8  16789  pythagtriplem9  16790  4sqlem10  16913  ram0  16988  cat1lem  18058  isipodrs  18498  chnub  18583  chnpof1  18591  gsumval2  18649  smndex1n0mnd  18878  smndex2dnrinv  18881  mulgnn  19046  sylow1lem1  19568  gsumval3eu  19874  ablsimpgfindlem1  20079  ablsimpgfindlem2  20080  ablsimpgfind  20082  fincygsubgodd  20084  submomnd  20102  rrgnz  20676  fidomndrng  20745  abvtrivd  20804  ornglmullt  20841  orngrmullt  20842  suborng  20848  00lss  20931  lvecvscan2  21106  prmirredlem  21466  ofldchr  21570  uvcff  21785  mvrcl  21984  mplmon  22027  mplmonmul  22028  psdmul  22146  coe1tmfv2  22254  cply1coe0  22280  cply1coe0bi  22281  1marepvsma1  22562  mdetrsca2  22583  mdetrlin2  22586  mdetunilem2  22592  mdetunilem5  22595  mdetunilem6  22596  mdetunilem9  22599  maducoeval2  22619  gsummatr01lem3  22636  gsummatr01lem4  22637  gsummatr01  22638  m2cpm  22720  m2cpminvid2lem  22733  fvmptnn04ifa  22829  fvmptnn04ifb  22830  fvmptnn04ifc  22831  chfacffsupp  22835  chfacfscmul0  22837  chfacfscmulgsum  22839  chfacfpmmul0  22841  chfacfpmmulgsum  22843  connclo  23394  dissnlocfin  23508  ptpjpre2  23559  txindis  23613  snfil  23843  alexsublem  24023  tsmsfbas  24107  stdbdxmet  24494  dscmet  24551  xrsxmet  24789  iccpnfcnv  24925  cphsubrglem  25158  minveclem3b  25409  minveclem4a  25411  ovolicc1  25497  dvexp2  25935  dvmptdiv  25955  lhop2  25996  deg1sublt  26089  ig1pval3  26157  dvply1  26264  plydiveu  26279  quotcan  26290  aaliou3lem9  26331  taylthlem2  26355  taylthlem2OLD  26356  pserdvlem2  26410  abelthlem9  26422  logccne0  26559  logtayllem  26640  logtayl  26641  cxpef  26646  rtprmirr  26741  angrtmuld  26789  isosctrlem3  26801  chordthmlem  26813  leibpilem2  26922  leibpi  26923  rlimcnp2  26947  efrlim  26950  efrlimOLD  26951  vma1  27147  muinv  27174  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  27920  elnnzs  28411  expnnsval  28436  expsne0  28446  bdayfinbndlem1  28477  tgbtwnne  28576  tgbtwndiff  28592  tgcolg  28640  tgbtwnconn1lem3  28660  legso  28685  tglineeltr  28717  tglineintmo  28728  tglineneq  28730  colline  28735  mirne  28753  miriso  28756  mirhl  28765  mirbtwnhl  28766  symquadlem  28775  krippenlem  28776  midexlem  28778  ragncol  28795  footexALT  28804  footexlem2  28806  colperp  28815  colperpexlem3  28818  mideulem2  28820  opphllem  28821  midex  28823  opptgdim2  28831  oppperpex  28839  hlpasch  28842  colopp  28855  lmieu  28870  trgcopy  28890  cgracol  28914  cgrg3col4  28939  axlowdimlem15  29043  axcontlem2  29052  axcontlem7  29057  1egrvtxdg0  29599  2pthnloop  29818  cyclnspth  29888  eupth2lem1  30307  eupth2lem2  30308  eupth2lem3lem6  30322  nrt2irr  30562  strlem6  32346  hstrlem6  32354  atssma  32468  chirredlem1  32480  snsssng  32603  ifnetrue  32636  ifnefals  32637  fmptunsnop  32792  xaddeq0  32845  rexmul2  32846  xlt2addrd  32851  xnn0nn0d  32864  hashpss  32901  elq2  32904  divnumden2  32908  sgnmul  32927  sgn0bi  32932  2exple2exp  32937  pmtridf1o  33174  pmtridfv1  33175  pmtridfv2  33176  elrgspnlem2  33323  elrgspnlem3  33324  domnprodeq0  33356  fracfld  33388  pidlnz  33455  lindssn  33457  drngidl  33512  drngidlhash  33513  0ringprmidl  33528  qsidomlem1  33531  ssdifidlprm  33537  mxidlmaxv  33547  mxidlprm  33549  mxidlirredi  33550  mxidlirred  33551  krull  33558  rsprprmprmidlb  33602  rprmasso2  33605  pidufd  33622  1arithufdlem3  33625  dfufd2  33629  zringidom  33630  0ringmon1p  33636  ig1pnunit  33680  mplmulmvr  33702  psrmonmul  33713  esplyfval2  33728  esplymhp  33731  esplyfval3  33735  vietadeg1  33741  lindsunlem  33788  fldextrspundgdvdslem  33844  fldext2rspun  33846  ply1annnr  33867  fldext2chn  33892  constrextdg2lem  33912  constrext2chnlem  33914  constrcon  33938  2sqr3minply  33944  cos9thpiminply  33952  1smat1  33968  submatminr1  33974  madjusmdetlem2  33992  zarcls1  34033  zarclsint  34036  zarclssn  34037  xrge0iifcnv  34097  xrge0iifcv  34098  xrge0iif1  34102  qqhval2lem  34145  qqhf  34150  qqhre  34184  esumrnmpt2  34232  esumcvgre  34255  inelpisys  34318  carsgclctunlem2  34483  ballotlemirc  34696  signswlid  34723  repr0  34775  reprlt  34783  reprgt  34785  reprinfz1  34786  tgoldbachgtda  34825  tgoldbachgt  34827  bnj1523  35233  acycgr2v  35352  fmlaomn0  35592  fmlasucdisj  35601  fz0n  35933  dfrdg2  35995  dfrdg4  36153  broutsideof2  36324  outsidele  36334  rankeq1o  36373  ivthALT  36537  limsucncmpi  36647  mh-inf3sn  36744  topdifinffinlem  37681  icorempo  37685  finxpreclem2  37724  finxp1o  37726  finxpreclem6  37730  poimirlem9  37968  poimirlem11  37970  poimirlem12  37971  poimirlem25  37984  fdc  38084  heibor1lem  38148  heiborlem4  38153  heiborlem6  38155  disjressuc2  38750  2atm  39991  lhpocnle  40480  lhp2at0nle  40499  trlval3  40651  cdleme18c  40757  cdlemg17b  41126  cdlemg17i  41133  dia2dimlem2  41529  dia2dimlem3  41530  dihord6apre  41720  dihatlat  41798  dochshpsat  41918  lcfrlem9  42014  mapdhval2  42190  hdmap1val2  42264  hdmap14lem4a  42335  hdmap14lem6  42337  dvrelogpow2b  42525  aks4d1p1p4  42528  aks4d1p6  42538  fldhmf1  42547  primrootspoweq0  42563  aks6d1c2p2  42576  hashscontpow  42579  aks6d1c5  42596  sticksstones1  42603  sticksstones10  42612  sticksstones12a  42614  sticksstones12  42615  sticksstones22  42625  aks6d1c6lem4  42630  aks6d1c7lem1  42637  aks6d1c7  42641  aks5lem8  42658  negn0nposznnd  42732  mhpind  43045  prjspner1  43077  dffltz  43085  3cubeslem2  43135  jm2.26lem3  43451  kelac1  43513  cantnfresb  43774  tfsconcat0b  43796  nlimsuc  43890  clsk1indlem0  44490  scotteld  44695  sineq0ALT  45385  refsum2cnlem1  45490  disjxp1  45522  disjf1  45635  disjrnmpt2  45640  disjinfi  45644  oddfl  45733  xrlttri5d  45739  supxrge  45790  nepnfltpnf  45794  nemnftgtmnft  45796  xrlexaddrp  45804  xrred  45816  supminfxr2  45919  icoiccdif  45976  qinioo  45987  ioonct  45989  fmul01lt1lem1  46036  climrec  46055  limcperiod  46080  reclimc  46103  limsupub  46154  liminflbuz2  46265  cncfiooicclem1  46343  cncfioobdlem  46346  fperdvper  46369  dvdivbd  46373  ditgeqiooicc  46410  itgsincmulx  46424  itgioocnicc  46427  iblcncfioo  46428  stoweidlem35  46485  stoweidlem39  46489  stirlinglem5  46528  stirlinglem8  46531  dirkerper  46546  dirkercncflem2  46554  dirkercncflem4  46556  fourierdlem31  46588  fourierdlem34  46591  fourierdlem41  46598  fourierdlem42  46599  fourierdlem44  46601  fourierdlem48  46604  fourierdlem49  46605  fourierdlem53  46609  fourierdlem56  46612  fourierdlem58  46614  fourierdlem60  46616  fourierdlem61  46617  fourierdlem62  46618  fourierdlem65  46621  fourierdlem66  46622  fourierdlem73  46629  fourierdlem76  46632  fourierdlem79  46635  fourierdlem81  46637  fourierdlem82  46638  fourierdlem93  46649  fourierdlem103  46659  fourierdlem104  46660  sqwvfoura  46678  fourierswlem  46680  elaa2lem  46683  elaa2  46684  etransclem4  46688  etransclem24  46708  etransclem31  46715  etransclem32  46716  etransclem35  46719  sge0repnf  46836  sge0fodjrnlem  46866  sge0iunmpt  46868  sge0rpcpnf  46871  nnfoctbdjlem  46905  meadjun  46912  voliunsge0lem  46922  hoicvr  46998  ovnn0val  47001  ovnsubaddlem1  47020  hoidmvn0val  47034  hsphoidmvle  47036  hoidmv1lelem1  47041  hoidmv1lelem2  47042  hoidmv1lelem3  47043  ovnhoilem1  47051  ovnsubadd2lem  47095  ovnovollem3  47108  cjnpoly  47353  lighneallem3  48086  divgcdoddALTV  48174  isubgr0uhgr  48365  usgrexmpl2trifr  48529  gpg5nbgrvtx03star  48572  gpg5nbgr3star  48573  dignn0flhalflem1  49107  itcoval2  49156  itcoval3  49157  itcovalsuc  49159  ackvalsuc1mpt  49170  line2xlem  49245