MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neneqd Structured version   Visualization version   GIF version

Theorem neneqd 2787
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
StepHypRef Expression
1 neneqd.1 . 2 (𝜑𝐴𝐵)
2 df-ne 2782 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
31, 2sylib 207 1 (𝜑 → ¬ 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1475  wne 2780
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 196  df-ne 2782
This theorem is referenced by:  neneq  2788  necon2bi  2812  necon2i  2816  necon4i  2817  pm2.21ddne  2866  nelrdva  3384  disjprg  4578  0inp0  4763  onnseq  7328  sniffsupp  8198  ackbij1lem15  8939  ttukeylem7  9220  fpwwe2lem13  9343  canthnumlem  9349  canthp1lem2  9354  recgt0  10746  elnnz  11264  xrnemnf  11827  xrnepnf  11828  fzprval  12271  fzodisjsn  12374  expnnval  12725  elprchashprn2  13045  relexpsucnnr  13613  relexp1g  13614  relexpuzrel  13640  sgnp  13678  fprodn0f  14561  ruclem12  14809  dvdsle  14870  nndvdslegcd  15065  gcdnncl  15067  divgcdnn  15074  sqgcd  15116  eucalgf  15134  eucalginv  15135  lcmgcdlem  15157  lcmftp  15187  lcmfunsnlem2lem1  15189  lcmfunsnlem2lem2  15190  qredeu  15210  rpdvds  15212  cncongr2  15220  divgcdodd  15260  divnumden  15294  divdenle  15295  phisum  15333  oddprm  15353  pythagtriplem4  15362  pythagtriplem8  15366  pythagtriplem9  15367  pythagtriplem19  15376  4sqlem10  15489  ram0  15564  isipodrs  16984  gsumval2  17103  mulgnn  17370  sylow1lem1  17836  gsumval3eu  18128  abvtrivd  18663  00lss  18763  lvecvscan2  18933  fidomndrng  19128  mvrcl  19270  mplmon  19284  mplmonmul  19285  evlslem3  19335  coe1tmfv2  19466  cply1coe0  19490  cply1coe0bi  19491  prmirredlem  19660  uvcff  19949  1marepvsma1  20208  mdetrsca2  20229  mdetrlin2  20232  mdetunilem2  20238  mdetunilem5  20241  mdetunilem6  20242  mdetunilem9  20245  maducoeval2  20265  gsummatr01lem3  20282  gsummatr01lem4  20283  gsummatr01  20284  m2cpm  20365  m2cpminvid2lem  20378  fvmptnn04ifa  20474  fvmptnn04ifb  20475  fvmptnn04ifc  20476  chfacffsupp  20480  chfacfscmul0  20482  chfacfscmulgsum  20484  chfacfpmmul0  20486  chfacfpmmulgsum  20488  conclo  21028  dissnlocfin  21142  ptpjpre2  21193  txindis  21247  snfil  21478  alexsublem  21658  tsmsfbas  21741  stdbdxmet  22130  dscmet  22187  xrsxmet  22420  iccpnfcnv  22551  cphsubrglem  22785  minveclem3b  23007  minveclem4a  23009  ovolicc1  23091  dvexp2  23523  lhop2  23582  deg1sublt  23674  ig1pval3  23738  dvply1  23843  plydiveu  23857  quotcan  23868  aaliou3lem9  23909  taylthlem2  23932  pserdvlem2  23986  abelthlem9  23998  logccne0  24129  logtayllem  24205  logtayl  24206  cxpef  24211  angrtmuld  24338  isosctrlem2  24349  isosctrlem3  24350  chordthmlem  24359  leibpilem2  24468  leibpi  24469  rlimcnp2  24493  efrlim  24496  vma1  24692  muinv  24719  lgsval2lem  24832  lgsval4  24842  lgsdir  24857  lgseisenlem4  24903  lgsquadlem1  24905  lgsquad2  24911  m1lgs  24913  2sqlem8a  24950  2sqlem8  24951  padicabv  25119  ostth1  25122  ostth3  25127  tgbtwnne  25185  tgbtwndiff  25201  tgcolg  25249  tgbtwnconn1lem3  25269  legso  25294  tglineeltr  25326  tglineintmo  25337  tglineneq  25339  colline  25344  mirne  25362  miriso  25365  mirhl  25374  mirbtwnhl  25375  symquadlem  25384  krippenlem  25385  midexlem  25387  ragncol  25404  footex  25413  colperp  25421  colperpexlem3  25424  mideulem2  25426  opphllem  25427  midex  25429  opptgdim2  25437  oppperpex  25445  hlpasch  25448  colopp  25461  colhp  25462  lmieu  25476  trgcopy  25496  cgracol  25519  cgrg3col4  25534  axlowdimlem15  25636  axcontlem2  25645  axcontlem7  25650  isusgra0  25876  usgraop  25879  usgra1v  25919  cyclnspth  26159  clwwlkn0  26302  rusgra0edg  26482  eupath2lem1  26504  eupath2lem2  26505  eupath2lem3  26506  strlem6  28499  hstrlem6  28507  atssma  28621  chirredlem1  28633  znsqcld  28900  xaddeq0  28907  xlt2addrd  28913  divnumden2  28951  2sqcoprm  28978  2sqmod  28979  submomnd  29041  ornglmullt  29138  orngrmullt  29139  ofldchr  29145  suborng  29146  1smat1  29198  submatminr1  29204  madjusmdetlem2  29222  xrge0iifcnv  29307  xrge0iifcv  29308  xrge0iif1  29312  qqhval2lem  29353  qqhf  29358  qqhre  29392  esumrnmpt2  29457  esumcvgre  29480  inelpisys  29544  carsgclctunlem2  29708  ballotlemirc  29920  sgnmul  29931  sgn0bi  29936  signswlid  29962  bnj1523  30393  fz0n  30869  dfrdg2  30945  nobndup  31099  nobnddown  31100  dfrdg4  31228  broutsideof2  31399  outsidele  31409  rankeq1o  31448  ivthALT  31500  limsucncmpi  31614  topdifinffinlem  32371  icorempt2  32375  finxpreclem2  32403  finxp1o  32405  finxpreclem6  32409  poimirlem9  32588  poimirlem11  32590  poimirlem12  32591  poimirlem25  32604  fdc  32711  heibor1lem  32778  heiborlem4  32783  heiborlem6  32785  2atm  33831  lhpocnle  34320  lhp2at0nle  34339  trlval3  34492  cdleme18c  34598  cdlemg17b  34968  cdlemg17i  34975  dia2dimlem2  35372  dia2dimlem3  35373  dihord6apre  35563  dihatlat  35641  dochshpsat  35761  lcfrlem9  35857  mapdhval2  36033  hdmap1val2  36108  hdmap14lem4a  36181  hdmap14lem6  36183  jm2.26lem3  36586  kelac1  36651  clsk3nimkb  37358  clsk1indlem0  37359  sineq0ALT  38195  refsum2cnlem1  38219  disjxp1  38263  nelrnmpt  38283  disjf1  38364  disjrnmpt2  38370  disjinfi  38375  rnmptn0  38408  oddfl  38430  xrlttri5d  38436  supxrge  38495  nepnfltpnf  38499  nemnftgtmnft  38501  xrlexaddrp  38509  xrred  38522  icoiccdif  38597  qinioo  38609  ioonct  38611  fmul01lt1lem1  38651  climrec  38670  limcperiod  38695  reclimc  38720  cncfiooicclem1  38779  cncfioobdlem  38782  dvmptdiv  38807  fperdvper  38808  dvdivbd  38813  ditgeqiooicc  38852  itgsincmulx  38866  itgioocnicc  38869  iblcncfioo  38870  stoweidlem35  38928  stoweidlem39  38932  stirlinglem5  38971  stirlinglem8  38974  dirkerper  38989  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem31  39031  fourierdlem34  39034  fourierdlem41  39041  fourierdlem42  39042  fourierdlem44  39044  fourierdlem48  39047  fourierdlem49  39048  fourierdlem53  39052  fourierdlem56  39055  fourierdlem58  39057  fourierdlem60  39059  fourierdlem61  39060  fourierdlem62  39061  fourierdlem65  39064  fourierdlem66  39065  fourierdlem73  39072  fourierdlem76  39075  fourierdlem79  39078  fourierdlem81  39080  fourierdlem82  39081  fourierdlem93  39092  fourierdlem103  39102  fourierdlem104  39103  sqwvfoura  39121  fourierswlem  39123  elaa2lem  39126  elaa2  39127  etransclem4  39131  etransclem24  39151  etransclem31  39158  etransclem32  39159  etransclem35  39162  sge0repnf  39279  sge0fodjrnlem  39309  sge0iunmpt  39311  sge0rpcpnf  39314  nnfoctbdjlem  39348  meadjun  39355  voliunsge0lem  39365  hoicvr  39438  ovnn0val  39441  ovnsubaddlem1  39460  hoidmvn0val  39474  hsphoidmvle  39476  hoidmv1lelem1  39481  hoidmv1lelem2  39482  hoidmv1lelem3  39483  ovnhoilem1  39491  ovnsubadd2lem  39535  ovnovollem3  39548  lighneallem3  40062  divgcdoddALTV  40131  1egrvtxdg0  40727  2pthnloop  40937  cyclnsPth  41006  eupth2lem1  41386  eupth2lem2  41387  eupth2lem3lem6  41401  dignn0flhalflem1  42207
  Copyright terms: Public domain W3C validator