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  3664  eldifsnneq  4748  disjprg  5095  0inp0  5305  nelrnmpt  5917  rnmptn0  6203  resf1extb  7878  frxp2  8088  frxp3  8095  onnseq  8278  finnzfsuppd  9280  sniffsupp  9307  dfac2b  10045  ackbij1lem15  10147  ttukeylem7  10429  fpwwe2lem12  10557  canthnumlem  10563  canthp1lem2  10568  recgt0  11991  nnneneg  12184  elnnz  12502  xrnemnf  13035  xrnepnf  13036  fzprval  13505  fzodisjsn  13617  fzone1  13704  expnnval  13991  znsqcld  14089  hashelne0d  14295  elprchashprn2  14323  relexpsucnnr  14952  relexp1g  14953  relexpuzrel  14979  sgnp  15017  fprodn0f  15918  ruclem12  16170  dvdsle  16241  nndvdslegcd  16436  gcdnncl  16438  divgcdnn  16446  nn0rppwr  16492  sqgcd  16493  eucalgf  16514  eucalginv  16515  lcmgcdlem  16537  lcmftp  16567  lcmfunsnlem2lem1  16569  lcmfunsnlem2lem2  16570  qredeu  16589  rpdvds  16591  cncongr2  16599  divnumden  16679  divdenle  16680  phisum  16722  oddprm  16742  pythagtriplem4  16751  pythagtriplem8  16755  pythagtriplem9  16756  4sqlem10  16879  ram0  16954  cat1lem  18024  isipodrs  18464  chnub  18549  chnpof1  18557  gsumval2  18615  smndex1n0mnd  18841  smndex2dnrinv  18844  mulgnn  19009  sylow1lem1  19531  gsumval3eu  19837  ablsimpgfindlem1  20042  ablsimpgfindlem2  20043  ablsimpgfind  20045  fincygsubgodd  20047  submomnd  20065  rrgnz  20641  fidomndrng  20710  abvtrivd  20769  ornglmullt  20806  orngrmullt  20807  suborng  20813  00lss  20896  lvecvscan2  21071  prmirredlem  21431  ofldchr  21535  uvcff  21750  mvrcl  21951  mplmon  21994  mplmonmul  21995  psdmul  22113  coe1tmfv2  22221  cply1coe0  22249  cply1coe0bi  22250  1marepvsma1  22531  mdetrsca2  22552  mdetrlin2  22555  mdetunilem2  22561  mdetunilem5  22564  mdetunilem6  22565  mdetunilem9  22568  maducoeval2  22588  gsummatr01lem3  22605  gsummatr01lem4  22606  gsummatr01  22607  m2cpm  22689  m2cpminvid2lem  22702  fvmptnn04ifa  22798  fvmptnn04ifb  22799  fvmptnn04ifc  22800  chfacffsupp  22804  chfacfscmul0  22806  chfacfscmulgsum  22808  chfacfpmmul0  22810  chfacfpmmulgsum  22812  connclo  23363  dissnlocfin  23477  ptpjpre2  23528  txindis  23582  snfil  23812  alexsublem  23992  tsmsfbas  24076  stdbdxmet  24463  dscmet  24520  xrsxmet  24758  iccpnfcnv  24902  cphsubrglem  25137  minveclem3b  25388  minveclem4a  25390  ovolicc1  25477  dvexp2  25918  dvmptdiv  25938  lhop2  25980  deg1sublt  26075  ig1pval3  26143  dvply1  26251  plydiveu  26266  quotcan  26277  aaliou3lem9  26318  taylthlem2  26342  taylthlem2OLD  26343  pserdvlem2  26398  abelthlem9  26410  logccne0  26547  logtayllem  26628  logtayl  26629  cxpef  26634  rtprmirr  26730  angrtmuld  26778  isosctrlem3  26790  chordthmlem  26802  leibpilem2  26911  leibpi  26912  rlimcnp2  26936  efrlim  26939  efrlimOLD  26940  vma1  27136  muinv  27163  lgsval2lem  27278  lgsval4  27288  lgsdir  27303  lgseisenlem4  27349  lgsquadlem1  27351  lgsquad2  27357  m1lgs  27359  2sqlem8a  27396  2sqlem8  27397  2sqcoprm  27406  2sqmod  27407  padicabv  27601  ostth1  27604  ostth3  27609  nolesgn2ores  27644  nogesgn1ores  27646  nosep1o  27653  nosep2o  27654  nosepdmlem  27655  nosepssdm  27658  noresle  27669  nosupbnd1lem3  27682  nosupbnd1lem4  27683  nosupbnd1lem5  27684  nosupbnd1lem6  27685  nosupbnd2lem1  27687  noinfbnd1lem3  27697  noinfbnd1lem4  27698  noinfbnd1lem5  27699  noinfbnd1lem6  27700  noinfbnd2lem1  27702  0elold  27910  elnnzs  28401  expnnsval  28426  expsne0  28436  bdayfinbndlem1  28467  tgbtwnne  28566  tgbtwndiff  28582  tgcolg  28630  tgbtwnconn1lem3  28650  legso  28675  tglineeltr  28707  tglineintmo  28718  tglineneq  28720  colline  28725  mirne  28743  miriso  28746  mirhl  28755  mirbtwnhl  28756  symquadlem  28765  krippenlem  28766  midexlem  28768  ragncol  28785  footexALT  28794  footexlem2  28796  colperp  28805  colperpexlem3  28808  mideulem2  28810  opphllem  28811  midex  28813  opptgdim2  28821  oppperpex  28829  hlpasch  28832  colopp  28845  lmieu  28860  trgcopy  28880  cgracol  28904  cgrg3col4  28929  axlowdimlem15  29033  axcontlem2  29042  axcontlem7  29047  1egrvtxdg0  29589  2pthnloop  29808  cyclnspth  29878  eupth2lem1  30297  eupth2lem2  30298  eupth2lem3lem6  30312  nrt2irr  30552  strlem6  32335  hstrlem6  32343  atssma  32457  chirredlem1  32469  snsssng  32592  ifnetrue  32625  ifnefals  32626  fmptunsnop  32781  xaddeq0  32835  rexmul2  32836  xlt2addrd  32841  xnn0nn0d  32854  hashpss  32891  elq2  32894  divnumden2  32898  sgnmul  32918  sgn0bi  32923  2exple2exp  32928  pmtridf1o  33178  pmtridfv1  33179  pmtridfv2  33180  elrgspnlem2  33327  elrgspnlem3  33328  domnprodeq0  33360  fracfld  33392  pidlnz  33459  lindssn  33461  drngidl  33516  drngidlhash  33517  0ringprmidl  33532  qsidomlem1  33535  ssdifidlprm  33541  mxidlmaxv  33551  mxidlprm  33553  mxidlirredi  33554  mxidlirred  33555  krull  33562  rsprprmprmidlb  33606  rprmasso2  33609  pidufd  33626  1arithufdlem3  33629  dfufd2  33633  zringidom  33634  0ringmon1p  33640  ig1pnunit  33684  mplmulmvr  33706  esplyfval2  33725  esplymhp  33728  esplyfval3  33732  vietadeg1  33736  lindsunlem  33783  fldextrspundgdvdslem  33839  fldext2rspun  33841  ply1annnr  33862  fldext2chn  33887  constrextdg2lem  33907  constrext2chnlem  33909  constrcon  33933  2sqr3minply  33939  cos9thpiminply  33947  1smat1  33963  submatminr1  33969  madjusmdetlem2  33987  zarcls1  34028  zarclsint  34031  zarclssn  34032  xrge0iifcnv  34092  xrge0iifcv  34093  xrge0iif1  34097  qqhval2lem  34140  qqhf  34145  qqhre  34179  esumrnmpt2  34227  esumcvgre  34250  inelpisys  34313  carsgclctunlem2  34478  ballotlemirc  34691  signswlid  34718  repr0  34770  reprlt  34778  reprgt  34780  reprinfz1  34781  tgoldbachgtda  34820  tgoldbachgt  34822  bnj1523  35229  acycgr2v  35346  fmlaomn0  35586  fmlasucdisj  35595  fz0n  35927  dfrdg2  35989  dfrdg4  36147  broutsideof2  36318  outsidele  36328  rankeq1o  36367  ivthALT  36531  limsucncmpi  36641  topdifinffinlem  37554  icorempo  37558  finxpreclem2  37597  finxp1o  37599  finxpreclem6  37603  poimirlem9  37832  poimirlem11  37834  poimirlem12  37835  poimirlem25  37848  fdc  37948  heibor1lem  38012  heiborlem4  38017  heiborlem6  38019  disjressuc2  38614  2atm  39855  lhpocnle  40344  lhp2at0nle  40363  trlval3  40515  cdleme18c  40621  cdlemg17b  40990  cdlemg17i  40997  dia2dimlem2  41393  dia2dimlem3  41394  dihord6apre  41584  dihatlat  41662  dochshpsat  41782  lcfrlem9  41878  mapdhval2  42054  hdmap1val2  42128  hdmap14lem4a  42199  hdmap14lem6  42201  dvrelogpow2b  42390  aks4d1p1p4  42393  aks4d1p6  42403  fldhmf1  42412  primrootspoweq0  42428  aks6d1c2p2  42441  hashscontpow  42444  aks6d1c5  42461  sticksstones1  42468  sticksstones10  42477  sticksstones12a  42479  sticksstones12  42480  sticksstones22  42490  aks6d1c6lem4  42495  aks6d1c7lem1  42502  aks6d1c7  42506  aks5lem8  42523  negn0nposznnd  42604  mhpind  42904  prjspner1  42936  dffltz  42944  3cubeslem2  42994  jm2.26lem3  43310  kelac1  43372  cantnfresb  43633  tfsconcat0b  43655  nlimsuc  43749  clsk1indlem0  44349  scotteld  44554  sineq0ALT  45244  refsum2cnlem1  45349  disjxp1  45381  disjf1  45494  disjrnmpt2  45499  disjinfi  45503  oddfl  45593  xrlttri5d  45599  supxrge  45650  nepnfltpnf  45654  nemnftgtmnft  45656  xrlexaddrp  45664  xrred  45676  supminfxr2  45780  icoiccdif  45837  qinioo  45848  ioonct  45850  fmul01lt1lem1  45897  climrec  45916  limcperiod  45941  reclimc  45964  limsupub  46015  liminflbuz2  46126  cncfiooicclem1  46204  cncfioobdlem  46207  fperdvper  46230  dvdivbd  46234  ditgeqiooicc  46271  itgsincmulx  46285  itgioocnicc  46288  iblcncfioo  46289  stoweidlem35  46346  stoweidlem39  46350  stirlinglem5  46389  stirlinglem8  46392  dirkerper  46407  dirkercncflem2  46415  dirkercncflem4  46417  fourierdlem31  46449  fourierdlem34  46452  fourierdlem41  46459  fourierdlem42  46460  fourierdlem44  46462  fourierdlem48  46465  fourierdlem49  46466  fourierdlem53  46470  fourierdlem56  46473  fourierdlem58  46475  fourierdlem60  46477  fourierdlem61  46478  fourierdlem62  46479  fourierdlem65  46482  fourierdlem66  46483  fourierdlem73  46490  fourierdlem76  46493  fourierdlem79  46496  fourierdlem81  46498  fourierdlem82  46499  fourierdlem93  46510  fourierdlem103  46520  fourierdlem104  46521  sqwvfoura  46539  fourierswlem  46541  elaa2lem  46544  elaa2  46545  etransclem4  46549  etransclem24  46569  etransclem31  46576  etransclem32  46577  etransclem35  46580  sge0repnf  46697  sge0fodjrnlem  46727  sge0iunmpt  46729  sge0rpcpnf  46732  nnfoctbdjlem  46766  meadjun  46773  voliunsge0lem  46783  hoicvr  46859  ovnn0val  46862  ovnsubaddlem1  46881  hoidmvn0val  46895  hsphoidmvle  46897  hoidmv1lelem1  46902  hoidmv1lelem2  46903  hoidmv1lelem3  46904  ovnhoilem1  46912  ovnsubadd2lem  46956  ovnovollem3  46969  cjnpoly  47202  lighneallem3  47920  divgcdoddALTV  47995  isubgr0uhgr  48186  usgrexmpl2trifr  48350  gpg5nbgrvtx03star  48393  gpg5nbgr3star  48394  dignn0flhalflem1  48928  itcoval2  48977  itcoval3  48978  itcovalsuc  48980  ackvalsuc1mpt  48991  line2xlem  49066