Theorem neneqd 2963

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   = wceq 1570   ≠ wne 2958

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-ne 2959

This theorem is used by:  neneq  2964  necon2bi  2988  necon2i  2992  necon4i  2993  pm2.21ddne  3042  mteqand  3049  nelrdva  3668  nrmod  3845  eldifsnneq  4759  disjprg  5105  0inp0  5329  nelrnmpt  5957  rnmptn0  6245  resf1extb  7927  frxp2  8136  frxp3  8143  onnseq  8327  finnzfsuppd  9329  sniffsupp  9356  scotteld  9872  dfac2b  10119  ackbij1lem15  10221  ttukeylem7  10503  fpwwe2lem12  10631  canthnumlem  10637  canthp1lem2  10642  recgt0  12065  nnneneg  12275  elnnz  12605  xrnemnf  13146  xrnepnf  13147  fzprval  13618  fzodisjsn  13731  fzone1  13818  expnnval  14105  znsqcld  14203  hashelne0d  14409  elprchashprn2  14437  hashpss  14451  relexpsucnnr  15067  relexp1g  15068  relexpuzrel  15094  sgnp  15132  sgn0bi  15145  sgnmul  15149  fprodn0f  16050  ruclem12  16301  dvdsle  16372  nndvdslegcd  16567  gcdnncl  16569  divgcdnn  16577  nn0rppwr  16623  sqgcd  16624  eucalgf  16645  eucalginv  16646  lcmgcdlem  16668  lcmftp  16698  lcmfunsnlem2lem1  16700  lcmfunsnlem2lem2  16701  qredeu  16720  rpdvds  16722  cncongr2  16730  divnumden  16811  divdenle  16812  phisum  16854  oddprm  16874  pythagtriplem4  16883  pythagtriplem8  16887  pythagtriplem9  16888  4sqlem10  17011  ram0  17086  cat1lem  18157  isipodrs  18597  chnub  18682  chnpof1  18690  gsumval2  18748  smndex1n0mnd  18978  smndex2dnrinv  18981  mulgnn  19145  sylow1lem1  19672  gsumval3eu  19978  ablsimpgfindlem1  20183  ablsimpgfindlem2  20184  ablsimpgfind  20186  fincygsubgodd  20188  submomnd  20206  rrgnz  20812  fidomndrng  20886  abvtrivd  20944  ornglmullt  20981  orngrmullt  20982  suborng  20988  00lss  21071  lvecvscan2  21245  pidlnz  21383  drngidl  21394  0ringprmidl  21486  qsidomlem1  21489  ssdifidlprm  21495  prmirredlem  21631  ofldchr  21735  uvcff  21950  mvrcl  22150  mplmon  22195  mplmonmul  22196  psdmul  22338  coe1tmfv2  22445  cply1coe0  22470  cply1coe0bi  22471  1marepvsma1  22749  mdetrsca2  22770  mdetrlin2  22773  mdetunilem2  22779  mdetunilem5  22782  mdetunilem6  22783  mdetunilem9  22786  maducoeval2  22806  gsummatr01lem3  22823  gsummatr01lem4  22824  gsummatr01  22825  m2cpm  22907  m2cpminvid2lem  22920  fvmptnn04ifa  23016  fvmptnn04ifb  23017  fvmptnn04ifc  23018  chfacffsupp  23022  chfacfscmul0  23024  chfacfscmulgsum  23026  chfacfpmmul0  23028  chfacfpmmulgsum  23030  connclo  23581  dissnlocfin  23695  ptpjpre2  23746  txindis  23800  snfil  24030  alexsublem  24210  tsmsfbas  24294  stdbdxmet  24681  dscmet  24738  xrsxmet  24976  iccpnfcnv  25112  cphsubrglem  25345  minveclem3b  25596  minveclem4a  25598  ovolicc1  25684  dvexp2  26122  dvmptdiv  26142  lhop2  26183  deg1sublt  26276  ig1pval3  26344  dvply1  26454  plydiveu  26468  quotcan  26479  aaliou3lem9  26522  taylthlem2  26546  pserdvlem2  26600  abelthlem9  26612  logccne0  26752  logtayllem  26833  logtayl  26834  cxpef  26839  rtprmirr  26934  angrtmuld  26982  isosctrlem3  26994  chordthmlem  27006  leibpilem2  27115  leibpi  27116  rlimcnp2  27140  efrlim  27143  vma1  27339  muinv  27366  lgsval2lem  27480  lgsval4  27490  lgsdir  27505  lgseisenlem4  27551  lgsquadlem1  27553  lgsquad2  27559  m1lgs  27561  2sqlem8a  27598  2sqlem8  27599  2sqcoprm  27608  2sqmod  27609  padicabv  27803  ostth1  27806  ostth3  27811  nolesgn2ores  27845  nogesgn1ores  27847  nosep1o  27854  nosep2o  27855  nosepdmlem  27856  nosepssdm  27859  noresle  27870  nosupbnd1lem3  27883  nosupbnd1lem4  27884  nosupbnd1lem5  27885  nosupbnd1lem6  27886  nosupbnd2lem1  27888  noinfbnd1lem3  27898  noinfbnd1lem4  27899  noinfbnd1lem5  27900  noinfbnd1lem6  27901  noinfbnd2lem1  27903  0elold  28112  elnnzs  28603  expnnsval  28628  expsne0  28638  bdayfinbndlem1  28669  tgbtwnne  28768  tgbtwndiff  28784  tgcolg  28832  tgbtwnconn1lem3  28852  legso  28877  tglineeltr  28913  tglineintmo  28924  tglineneq  28927  colline  28932  tglnpt4  28937  mirne  28953  miriso  28956  mirhl  28965  mirbtwnhl  28966  symquadlem  28975  krippenlem  28976  midexlem  28978  symquadprlnglem  28979  ragncol  28998  footexALT  29007  footexlem2  29009  colperp  29019  colperpexlem3  29022  mideulem2  29024  opphllem  29025  midex  29027  opptgdim2  29035  oppperpex  29043  hlpasch  29047  colopp  29060  lnincplng  29075  plngrotlem1  29078  plngrotlem2  29079  lnssplnglem  29082  lnssplng  29083  lmieu  29102  trgcopy  29124  cgracol  29148  cgrg3col4  29179  prlngin0  29203  prlngpln  29204  prlnghpg  29205  dfprlng2  29206  prlngex  29210  prlngmolem1  29211  prlngmolem2  29212  prlngmo2  29215  prlngpln4  29217  prlnginn0  29219  prlngmid2  29220  prlngsymquadlem  29222  tgaltai  29226  axlowdimlem15  29315  axcontlem2  29324  axcontlem7  29329  1egrvtxdg0  29870  2pthnloop  30089  cyclnspth  30159  eupth2lem1  30578  eupth2lem2  30579  eupth2lem3lem6  30593  nrt2irr  30833  strlem6  32617  hstrlem6  32625  atssma  32739  chirredlem1  32751  snsssng  32869  ifnetrue  32902  ifnefals  32903  fmptunsnop  33054  xaddeq0  33107  rexmul2  33108  xlt2addrd  33113  xnn0nn0d  33126  elq2  33165  divnumden2  33169  2exple2exp  33187  pmtridf1o  33423  pmtridfv1  33424  pmtridfv2  33425  elrgspnlem2  33572  elrgspnlem3  33573  domnprodeq0  33608  fracfld  33638  lindssn  33700  drngidlhash  33750  mxidlmaxv  33760  mxidlprm  33762  mxidlirredi  33763  mxidlirred  33764  krull  33770  drnglring  33791  dflring3  33796  dflring4  33797  rsprprmprmidlb  33822  rprmasso2  33825  pidufd  33842  1arithufdlem3  33845  dfufd2  33849  zringidom  33850  0ringmon1p  33856  ig1pnunit  33900  mplmulmvr  33938  psrmonmul  33949  esplyfval2  33964  esplymhp  33967  esplyfval3  33971  vietadeg1  33977  lindsunlem  34023  fldextrspundgdvdslem  34079  fldext2rspun  34081  ply1annnr  34102  fldext2chn  34127  constrextdg2lem  34147  constrext2chnlem  34149  constrcon  34173  2sqr3minply  34179  cos9thpiminply  34187  1smat1  34203  submatminr1  34209  madjusmdetlem2  34227  zarcls1  34268  zarclsint  34271  zarclssn  34272  xrge0iifcnv  34332  xrge0iifcv  34333  xrge0iif1  34337  qqhval2lem  34380  qqhf  34385  qqhre  34419  esumrnmpt2  34467  esumcvgre  34490  inelpisys  34553  carsgclctunlem2  34718  ballotlemirc  34931  signswlid  34955  repr0  35007  reprlt  35015  reprgt  35017  reprinfz1  35018  tgoldbachgtda  35057  tgoldbachgt  35059  bnj1523  35468  kard0b  35580  acycgr2v  35650  fmlaomn0  35890  fmlasucdisj  35899  fz0n  36231  dfrdg2  36293  dfrdg4  36451  broutsideof2  36622  outsidele  36632  rankeq1o  36671  ivthALT  36874  limsucncmpi  36984  mh-inf3sn  37081  qdiff  37999  topdifinffinlem  38021  icorempo  38025  finxpreclem2  38064  finxp1o  38066  finxpreclem6  38070  poimirlem9  38308  poimirlem11  38310  poimirlem12  38311  poimirlem25  38324  fdc  38424  heibor1lem  38488  heiborlem4  38493  heiborlem6  38495  disjressuc2  39088  2atm  40329  lhpocnle  40818  lhp2at0nle  40837  trlval3  40989  cdleme18c  41095  cdlemg17b  41464  cdlemg17i  41471  dia2dimlem2  41867  dia2dimlem3  41868  dihord6apre  42058  dihatlat  42136  dochshpsat  42256  lcfrlem9  42352  mapdhval2  42528  hdmap1val2  42602  hdmap14lem4a  42673  hdmap14lem6  42675  dvrelogpow2b  42863  aks4d1p1p4  42866  aks4d1p6  42876  fldhmf1  42885  primrootspoweq0  42901  aks6d1c2p2  42914  hashscontpow  42917  aks6d1c5  42934  sticksstones1  42941  sticksstones10  42950  sticksstones12a  42952  sticksstones12  42953  sticksstones22  42963  aks6d1c6lem4  42968  aks6d1c7lem1  42975  aks6d1c7  42979  aks5lem8  42996  quadfac  43000  negn0nposznnd  43071  mhpind  43354  prjspner1  43386  dffltz  43394  3cubeslem2  43444  jm2.26lem3  43756  kelac1  43818  cantnfresb  44079  tfsconcat0b  44101  nlimsuc  44195  clsk1indlem0  44795  sineq0ALT  45673  refsum2cnlem1  45785  disjxp1  45817  disjf1  45929  disjrnmpt2  45934  disjinfi  45938  oddfl  46025  xrlttri5d  46031  supxrge  46082  nepnfltpnf  46086  nemnftgtmnft  46088  xrlexaddrp  46096  xrred  46108  supminfxr2  46211  icoiccdif  46268  qinioo  46279  ioonct  46281  fmul01lt1lem1  46328  climrec  46347  limcperiod  46372  reclimc  46395  limsupub  46446  liminflbuz2  46557  cncfiooicclem1  46635  cncfioobdlem  46638  fperdvper  46661  dvdivbd  46665  ditgeqiooicc  46702  itgsincmulx  46716  itgioocnicc  46719  iblcncfioo  46720  stoweidlem35  46777  stoweidlem39  46781  stirlinglem5  46820  stirlinglem8  46823  dirkerper  46838  dirkercncflem2  46846  dirkercncflem4  46848  fourierdlem31  46880  fourierdlem34  46883  fourierdlem41  46890  fourierdlem42  46891  fourierdlem44  46893  fourierdlem48  46896  fourierdlem49  46897  fourierdlem53  46901  fourierdlem56  46904  fourierdlem58  46906  fourierdlem60  46908  fourierdlem61  46909  fourierdlem62  46910  fourierdlem65  46913  fourierdlem66  46914  fourierdlem73  46921  fourierdlem76  46924  fourierdlem79  46927  fourierdlem81  46929  fourierdlem82  46930  fourierdlem93  46941  fourierdlem103  46951  fourierdlem104  46952  sqwvfoura  46970  fourierswlem  46972  elaa2lem  46975  elaa2  46976  etransclem4  46980  etransclem24  47000  etransclem31  47007  etransclem32  47008  etransclem35  47011  sge0repnf  47128  sge0fodjrnlem  47158  sge0iunmpt  47160  sge0rpcpnf  47163  nnfoctbdjlem  47197  meadjun  47204  voliunsge0lem  47214  hoicvr  47290  ovnn0val  47293  ovnsubaddlem1  47312  hoidmvn0val  47326  hsphoidmvle  47328  hoidmv1lelem1  47333  hoidmv1lelem2  47334  hoidmv1lelem3  47335  ovnhoilem1  47343  ovnsubadd2lem  47387  ovnovollem3  47400  cjnpoly  47654  lighneallem3  48387  divgcdoddALTV  48475  isubgr0uhgr  48666  usgrexmpl2trifr  48830  gpg5nbgrvtx03star  48873  gpg5nbgr3star  48874  smprngprmrng  49132  dignn0flhalflem1  49423  itcoval2  49472  itcoval3  49473  itcovalsuc  49475  ackvalsuc1mpt  49486  line2xlem  49561