Theorem neneqd 2973

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

Syntax hints:  ¬ wn 3   → wi 4   = wceq 1507   ≠ wne 2968

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 199  df-ne 2969

This theorem is referenced by:  neneq  2974  necon2bi  2998  necon2i  3002  necon4i  3003  pm2.21ddne  3053  nelrdva  3611  eldifsnneq  4597  disjprg  4925  0inp0  5113  onnseq  7785  sniffsupp  8668  dfac2b  9350  ackbij1lem15  9454  ttukeylem7  9735  fpwwe2lem13  9862  canthnumlem  9868  canthp1lem2  9873  recgt0  11287  nnneneg  11475  elnnz  11803  xrnemnf  12329  xrnepnf  12330  fzprval  12784  fzodisjsn  12890  expnnval  13247  znsqcld  13341  elprchashprn2  13570  relexpsucnnr  14245  relexp1g  14246  relexpuzrel  14272  sgnp  14310  fprodn0f  15205  ruclem12  15454  dvdsle  15520  nndvdslegcd  15714  gcdnncl  15716  divgcdnn  15723  sqgcd  15765  eucalgf  15783  eucalginv  15784  lcmgcdlem  15806  lcmftp  15836  lcmfunsnlem2lem1  15838  lcmfunsnlem2lem2  15839  qredeu  15858  rpdvds  15860  cncongr2  15868  divnumden  15944  divdenle  15945  phisum  15983  oddprm  16003  pythagtriplem4  16012  pythagtriplem8  16016  pythagtriplem9  16017  4sqlem10  16139  ram0  16214  isipodrs  17629  gsumval2  17748  mulgnn  18019  sylow1lem1  18484  gsumval3eu  18778  abvtrivd  19333  00lss  19435  lvecvscan2  19606  fidomndrng  19801  mvrcl  19943  mplmon  19957  mplmonmul  19958  evlslem3  20007  coe1tmfv2  20146  cply1coe0  20170  cply1coe0bi  20171  prmirredlem  20342  uvcff  20637  1marepvsma1  20896  mdetrsca2  20917  mdetrlin2  20920  mdetunilem2  20926  mdetunilem5  20929  mdetunilem6  20930  mdetunilem9  20933  maducoeval2  20953  gsummatr01lem3  20970  gsummatr01lem4  20971  gsummatr01  20972  m2cpm  21053  m2cpminvid2lem  21066  fvmptnn04ifa  21162  fvmptnn04ifb  21163  fvmptnn04ifc  21164  chfacffsupp  21168  chfacfscmul0  21170  chfacfscmulgsum  21172  chfacfpmmul0  21174  chfacfpmmulgsum  21176  connclo  21727  dissnlocfin  21841  ptpjpre2  21892  txindis  21946  snfil  22176  alexsublem  22356  tsmsfbas  22439  stdbdxmet  22828  dscmet  22885  xrsxmet  23120  iccpnfcnv  23251  cphsubrglem  23484  minveclem3b  23734  minveclem4a  23736  ovolicc1  23820  dvexp2  24254  dvmptdiv  24274  lhop2  24315  deg1sublt  24407  ig1pval3  24471  dvply1  24576  plydiveu  24590  quotcan  24601  aaliou3lem9  24642  taylthlem2  24665  pserdvlem2  24719  abelthlem9  24731  logccne0  24863  logtayllem  24943  logtayl  24944  cxpef  24949  angrtmuld  25087  isosctrlem3  25099  chordthmlem  25111  leibpilem2  25221  leibpi  25222  rlimcnp2  25246  efrlim  25249  vma1  25445  muinv  25472  lgsval2lem  25585  lgsval4  25595  lgsdir  25610  lgseisenlem4  25656  lgsquadlem1  25658  lgsquad2  25664  m1lgs  25666  2sqlem8a  25703  2sqlem8  25704  2sqcoprm  25713  2sqmod  25714  padicabv  25908  ostth1  25911  ostth3  25916  tgbtwnne  25978  tgbtwndiff  25994  tgcolg  26042  tgbtwnconn1lem3  26062  legso  26087  tglineeltr  26119  tglineintmo  26130  tglineneq  26132  colline  26137  mirne  26155  miriso  26158  mirhl  26167  mirbtwnhl  26168  symquadlem  26177  krippenlem  26178  midexlem  26180  ragncol  26197  footexALT  26206  footexlem2  26208  colperp  26217  colperpexlem3  26220  mideulem2  26222  opphllem  26223  midex  26225  opptgdim2  26233  oppperpex  26241  hlpasch  26244  colopp  26257  lmieu  26272  trgcopy  26292  cgracol  26316  cgrg3col4  26342  axlowdimlem15  26445  axcontlem2  26454  axcontlem7  26459  1egrvtxdg0  26996  2pthnloop  27220  cyclnspth  27289  eupth2lem1  27748  eupth2lem2  27749  eupth2lem3lem6  27763  strlem6  29814  hstrlem6  29822  atssma  29936  chirredlem1  29948  xaddeq0  30229  xlt2addrd  30234  divnumden2  30280  submomnd  30426  cycpmfv1  30444  ornglmullt  30556  orngrmullt  30557  ofldchr  30563  suborng  30564  lindssn  30607  lindsunlem  30646  pmtridf1o  30694  pmtridfv1  30695  pmtridfv2  30696  1smat1  30708  submatminr1  30714  madjusmdetlem2  30732  xrge0iifcnv  30817  xrge0iifcv  30818  xrge0iif1  30822  qqhval2lem  30863  qqhf  30868  qqhre  30902  esumrnmpt2  30968  esumcvgre  30991  inelpisys  31055  carsgclctunlem2  31219  ballotlemirc  31432  sgnmul  31443  sgn0bi  31448  signswlid  31472  repr0  31527  reprlt  31535  reprgt  31537  reprinfz1  31538  tgoldbachgtda  31577  tgoldbachgt  31579  bnj1523  31985  fz0n  32479  dfrdg2  32558  nolesgn2ores  32697  nosep1o  32704  nosepdmlem  32705  nosepssdm  32708  noresle  32718  nosupbnd1lem3  32728  nosupbnd1lem4  32729  nosupbnd1lem5  32730  nosupbnd1lem6  32731  nosupbnd2lem1  32733  dfrdg4  32930  broutsideof2  33101  outsidele  33111  rankeq1o  33150  ivthALT  33201  limsucncmpi  33310  topdifinffinlem  34067  icorempo  34071  finxpreclem2  34109  finxp1o  34111  finxpreclem6  34115  poimirlem9  34339  poimirlem11  34341  poimirlem12  34342  poimirlem25  34355  fdc  34459  heibor1lem  34526  heiborlem4  34531  heiborlem6  34533  2atm  36105  lhpocnle  36594  lhp2at0nle  36613  trlval3  36765  cdleme18c  36871  cdlemg17b  37240  cdlemg17i  37247  dia2dimlem2  37643  dia2dimlem3  37644  dihord6apre  37834  dihatlat  37912  dochshpsat  38032  lcfrlem9  38128  mapdhval2  38304  hdmap1val2  38378  hdmap14lem4a  38449  hdmap14lem6  38451  mteqand  38546  negn0nposznnd  38597  nn0rppwr  38611  rtprmirr  38623  dffltz  38675  jm2.26lem3  38991  kelac1  39056  clsk3nimkb  39750  clsk1indlem0  39751  hashelne0d  39931  scotteld  39954  ablsimpgfindlem1  40040  ablsimpgfindlem2  40041  ablsimpgfind  40042  fincygsubgodd  40044  sineq0ALT  40687  refsum2cnlem1  40710  disjxp1  40748  nelrnmpt  40765  disjf1  40865  disjrnmpt2  40871  disjinfi  40876  rnmptn0  40907  oddfl  40970  xrlttri5d  40976  supxrge  41033  nepnfltpnf  41037  nemnftgtmnft  41039  xrlexaddrp  41047  xrred  41060  supminfxr2  41174  icoiccdif  41229  qinioo  41240  ioonct  41242  fmul01lt1lem1  41294  climrec  41313  limcperiod  41338  reclimc  41363  limsupub  41414  liminflbuz2  41525  cncfiooicclem1  41604  cncfioobdlem  41607  fperdvper  41631  dvdivbd  41636  ditgeqiooicc  41673  itgsincmulx  41687  itgioocnicc  41690  iblcncfioo  41691  stoweidlem35  41749  stoweidlem39  41753  stirlinglem5  41792  stirlinglem8  41795  dirkerper  41810  dirkercncflem2  41818  dirkercncflem4  41820  fourierdlem31  41852  fourierdlem34  41855  fourierdlem41  41862  fourierdlem42  41863  fourierdlem44  41865  fourierdlem48  41868  fourierdlem49  41869  fourierdlem53  41873  fourierdlem56  41876  fourierdlem58  41878  fourierdlem60  41880  fourierdlem61  41881  fourierdlem62  41882  fourierdlem65  41885  fourierdlem66  41886  fourierdlem73  41893  fourierdlem76  41896  fourierdlem79  41899  fourierdlem81  41901  fourierdlem82  41902  fourierdlem93  41913  fourierdlem103  41923  fourierdlem104  41924  sqwvfoura  41942  fourierswlem  41944  elaa2lem  41947  elaa2  41948  etransclem4  41952  etransclem24  41972  etransclem31  41979  etransclem32  41980  etransclem35  41983  sge0repnf  42097  sge0fodjrnlem  42127  sge0iunmpt  42129  sge0rpcpnf  42132  nnfoctbdjlem  42166  meadjun  42173  voliunsge0lem  42183  hoicvr  42259  ovnn0val  42262  ovnsubaddlem1  42281  hoidmvn0val  42295  hsphoidmvle  42297  hoidmv1lelem1  42302  hoidmv1lelem2  42303  hoidmv1lelem3  42304  ovnhoilem1  42312  ovnsubadd2lem  42356  ovnovollem3  42369  lighneallem3  43138  divgcdoddALTV  43213  dignn0flhalflem1  44041  line2xlem  44106