Theorem neneqd 2945

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1541   ≠ wne 2940

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 206  df-ne 2941

This theorem is referenced by:  neneq  2946  necon2bi  2971  necon2i  2975  necon4i  2976  pm2.21ddne  3026  mteqand  3033  nelrdva  3700  eldifsnneq  4793  disjprg  5143  0inp0  5356  rnmptn0  6240  frxp2  8126  frxp3  8133  onnseq  8340  sniffsupp  9391  dfac2b  10121  ackbij1lem15  10225  ttukeylem7  10506  fpwwe2lem12  10633  canthnumlem  10639  canthp1lem2  10644  recgt0  12056  nnneneg  12243  elnnz  12564  xrnemnf  13093  xrnepnf  13094  fzprval  13558  fzodisjsn  13666  expnnval  14026  znsqcld  14123  hashelne0d  14324  elprchashprn2  14352  relexpsucnnr  14968  relexp1g  14969  relexpuzrel  14995  sgnp  15033  fprodn0f  15931  ruclem12  16180  dvdsle  16249  nndvdslegcd  16442  gcdnncl  16444  divgcdnn  16452  sqgcd  16498  eucalgf  16516  eucalginv  16517  lcmgcdlem  16539  lcmftp  16569  lcmfunsnlem2lem1  16571  lcmfunsnlem2lem2  16572  qredeu  16591  rpdvds  16593  cncongr2  16601  divnumden  16680  divdenle  16681  phisum  16719  oddprm  16739  pythagtriplem4  16748  pythagtriplem8  16752  pythagtriplem9  16753  4sqlem10  16876  ram0  16951  cat1lem  18042  isipodrs  18486  gsumval2  18601  smndex1n0mnd  18789  smndex2dnrinv  18792  mulgnn  18952  sylow1lem1  19460  gsumval3eu  19766  ablsimpgfindlem1  19971  ablsimpgfindlem2  19972  ablsimpgfind  19974  fincygsubgodd  19976  abvtrivd  20440  00lss  20544  lvecvscan2  20717  fidomndrng  20918  prmirredlem  21033  uvcff  21337  mvrcl  21542  mplmon  21581  mplmonmul  21582  coe1tmfv2  21788  cply1coe0  21814  cply1coe0bi  21815  1marepvsma1  22076  mdetrsca2  22097  mdetrlin2  22100  mdetunilem2  22106  mdetunilem5  22109  mdetunilem6  22110  mdetunilem9  22113  maducoeval2  22133  gsummatr01lem3  22150  gsummatr01lem4  22151  gsummatr01  22152  m2cpm  22234  m2cpminvid2lem  22247  fvmptnn04ifa  22343  fvmptnn04ifb  22344  fvmptnn04ifc  22345  chfacffsupp  22349  chfacfscmul0  22351  chfacfscmulgsum  22353  chfacfpmmul0  22355  chfacfpmmulgsum  22357  connclo  22910  dissnlocfin  23024  ptpjpre2  23075  txindis  23129  snfil  23359  alexsublem  23539  tsmsfbas  23623  stdbdxmet  24015  dscmet  24072  xrsxmet  24316  iccpnfcnv  24451  cphsubrglem  24685  minveclem3b  24936  minveclem4a  24938  ovolicc1  25024  dvexp2  25462  dvmptdiv  25482  lhop2  25523  deg1sublt  25619  ig1pval3  25683  dvply1  25788  plydiveu  25802  quotcan  25813  aaliou3lem9  25854  taylthlem2  25877  pserdvlem2  25931  abelthlem9  25943  logccne0  26078  logtayllem  26158  logtayl  26159  cxpef  26164  angrtmuld  26302  isosctrlem3  26314  chordthmlem  26326  leibpilem2  26435  leibpi  26436  rlimcnp2  26460  efrlim  26463  vma1  26659  muinv  26686  lgsval2lem  26799  lgsval4  26809  lgsdir  26824  lgseisenlem4  26870  lgsquadlem1  26872  lgsquad2  26878  m1lgs  26880  2sqlem8a  26917  2sqlem8  26918  2sqcoprm  26927  2sqmod  26928  padicabv  27122  ostth1  27125  ostth3  27130  nolesgn2ores  27164  nogesgn1ores  27166  nosep1o  27173  nosep2o  27174  nosepdmlem  27175  nosepssdm  27178  noresle  27189  nosupbnd1lem3  27202  nosupbnd1lem4  27203  nosupbnd1lem5  27204  nosupbnd1lem6  27205  nosupbnd2lem1  27207  noinfbnd1lem3  27217  noinfbnd1lem4  27218  noinfbnd1lem5  27219  noinfbnd1lem6  27220  noinfbnd2lem1  27222  0elold  27391  tgbtwnne  27730  tgbtwndiff  27746  tgcolg  27794  tgbtwnconn1lem3  27814  legso  27839  tglineeltr  27871  tglineintmo  27882  tglineneq  27884  colline  27889  mirne  27907  miriso  27910  mirhl  27919  mirbtwnhl  27920  symquadlem  27929  krippenlem  27930  midexlem  27932  ragncol  27949  footexALT  27958  footexlem2  27960  colperp  27969  colperpexlem3  27972  mideulem2  27974  opphllem  27975  midex  27977  opptgdim2  27985  oppperpex  27993  hlpasch  27996  colopp  28009  lmieu  28024  trgcopy  28044  cgracol  28068  cgrg3col4  28093  axlowdimlem15  28203  axcontlem2  28212  axcontlem7  28217  1egrvtxdg0  28757  2pthnloop  28977  cyclnspth  29046  eupth2lem1  29460  eupth2lem2  29461  eupth2lem3lem6  29475  strlem6  31496  hstrlem6  31504  atssma  31618  chirredlem1  31630  snsssng  31739  ifnetrue  31766  ifnefals  31767  xaddeq0  31953  xlt2addrd  31958  fzone1  31998  divnumden2  32011  submomnd  32215  pmtridf1o  32240  pmtridfv1  32241  pmtridfv2  32242  ornglmullt  32413  orngrmullt  32414  ofldchr  32420  suborng  32421  pidlnz  32476  lindssn  32482  drngidl  32539  drngidlhash  32540  0ringprmidl  32556  qsidomlem1  32559  mxidlmaxv  32572  mxidlprm  32574  mxidlirredi  32575  mxidlirred  32576  krull  32582  0ringmon1p  32624  ig1pnunit  32658  lindsunlem  32697  ply1annnr  32752  1smat1  32772  submatminr1  32778  madjusmdetlem2  32796  zarcls1  32837  zarclsint  32840  zarclssn  32841  xrge0iifcnv  32901  xrge0iifcv  32902  xrge0iif1  32906  qqhval2lem  32949  qqhf  32954  qqhre  32988  esumrnmpt2  33054  esumcvgre  33077  inelpisys  33140  carsgclctunlem2  33306  ballotlemirc  33518  sgnmul  33529  sgn0bi  33534  signswlid  33558  repr0  33611  reprlt  33619  reprgt  33621  reprinfz1  33622  tgoldbachgtda  33661  tgoldbachgt  33663  bnj1523  34070  acycgr2v  34129  fmlaomn0  34369  fmlasucdisj  34378  fz0n  34688  dfrdg2  34755  dfrdg4  34911  broutsideof2  35082  outsidele  35092  rankeq1o  35131  ivthALT  35208  limsucncmpi  35318  topdifinffinlem  36216  icorempo  36220  finxpreclem2  36259  finxp1o  36261  finxpreclem6  36265  poimirlem9  36485  poimirlem11  36487  poimirlem12  36488  poimirlem25  36501  fdc  36601  heibor1lem  36665  heiborlem4  36670  heiborlem6  36672  disjressuc2  37246  2atm  38386  lhpocnle  38875  lhp2at0nle  38894  trlval3  39046  cdleme18c  39152  cdlemg17b  39521  cdlemg17i  39528  dia2dimlem2  39924  dia2dimlem3  39925  dihord6apre  40115  dihatlat  40193  dochshpsat  40313  lcfrlem9  40409  mapdhval2  40585  hdmap1val2  40659  hdmap14lem4a  40730  hdmap14lem6  40732  dvrelogpow2b  40921  aks4d1p1p4  40924  aks4d1p6  40934  fldhmf1  40943  aks6d1c2p2  40945  sticksstones1  40950  sticksstones10  40959  sticksstones12a  40961  sticksstones12  40962  sticksstones22  40972  metakunt6  40978  metakunt7  40979  metakunt11  40983  metakunt12  40984  metakunt27  40999  metakunt28  41000  metakunt29  41001  metakunt30  41002  mhpind  41163  negn0nposznnd  41191  nn0rppwr  41219  rtprmirr  41233  prjspner1  41364  dffltz  41372  3cubeslem2  41408  jm2.26lem3  41725  kelac1  41790  cantnfresb  42059  tfsconcat0b  42081  nlimsuc  42177  clsk1indlem0  42777  finnzfsuppd  42946  scotteld  42990  sineq0ALT  43683  refsum2cnlem1  43706  disjxp1  43741  nelrnmpt  43758  disjf1  43865  disjrnmpt2  43871  disjinfi  43876  oddfl  43973  xrlttri5d  43979  supxrge  44034  nepnfltpnf  44038  nemnftgtmnft  44040  xrlexaddrp  44048  xrred  44061  supminfxr2  44165  icoiccdif  44223  qinioo  44234  ioonct  44236  fmul01lt1lem1  44286  climrec  44305  limcperiod  44330  reclimc  44355  limsupub  44406  liminflbuz2  44517  cncfiooicclem1  44595  cncfioobdlem  44598  fperdvper  44621  dvdivbd  44625  ditgeqiooicc  44662  itgsincmulx  44676  itgioocnicc  44679  iblcncfioo  44680  stoweidlem35  44737  stoweidlem39  44741  stirlinglem5  44780  stirlinglem8  44783  dirkerper  44798  dirkercncflem2  44806  dirkercncflem4  44808  fourierdlem31  44840  fourierdlem34  44843  fourierdlem41  44850  fourierdlem42  44851  fourierdlem44  44853  fourierdlem48  44856  fourierdlem49  44857  fourierdlem53  44861  fourierdlem56  44864  fourierdlem58  44866  fourierdlem60  44868  fourierdlem61  44869  fourierdlem62  44870  fourierdlem65  44873  fourierdlem66  44874  fourierdlem73  44881  fourierdlem76  44884  fourierdlem79  44887  fourierdlem81  44889  fourierdlem82  44890  fourierdlem93  44901  fourierdlem103  44911  fourierdlem104  44912  sqwvfoura  44930  fourierswlem  44932  elaa2lem  44935  elaa2  44936  etransclem4  44940  etransclem24  44960  etransclem31  44967  etransclem32  44968  etransclem35  44971  sge0repnf  45088  sge0fodjrnlem  45118  sge0iunmpt  45120  sge0rpcpnf  45123  nnfoctbdjlem  45157  meadjun  45164  voliunsge0lem  45174  hoicvr  45250  ovnn0val  45253  ovnsubaddlem1  45272  hoidmvn0val  45286  hsphoidmvle  45288  hoidmv1lelem1  45293  hoidmv1lelem2  45294  hoidmv1lelem3  45295  ovnhoilem1  45303  ovnsubadd2lem  45347  ovnovollem3  45360  lighneallem3  46261  divgcdoddALTV  46336  dignn0flhalflem1  47254  itcoval2  47303  itcoval3  47304  itcovalsuc  47306  ackvalsuc1mpt  47317  line2xlem  47392