Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqneqall Unicode version

Theorem eqneqall 2664
 Description: A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
Assertion
Ref Expression
eqneqall

Proof of Theorem eqneqall
StepHypRef Expression
1 df-ne 2654 . 2
2 pm2.24 109 . 2
31, 2syl5bi 217 1
 Colors of variables: wff setvar class Syntax hints:  -.wn 3  ->wi 4  =wceq 1395  =/=wne 2652 This theorem is referenced by:  nonconne  2665  prnebg  4212  elovmpt3imp  6533  bropopvvv  6880  fin1a2lem10  8810  suppssfz  12100  hashrabsn1  12442  hash2prd  12518  hash2pwpr  12519  cshwidxmod  12774  cshwidx0  12776  symgextf1  16446  01eq0ring  17920  mamufacex  18891  mavmulsolcl  19053  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  usgra2edg  24382  wlk0  24761  clwwlkgt0  24771  clwwlknprop  24772  nbhashuvtx1  24915  rusgrasn  24945  frgrawopreglem4  25047  frgraregord13  25119  frgraogt3nreg  25120  tpres  32554  lidldomn1  32727  nzerooringczr  32880  ztprmneprm  32936  suppmptcfin  32972  linc1  33026  lindsrng01  33069  ldepspr  33074  zlmodzxznm  33098 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 185  df-ne 2654
 Copyright terms: Public domain W3C validator