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

Step	Hyp	Ref	Expression
1		df-ne 2654	. 2
2		pm2.24 109	. 2
3	1, 2	syl5bi 217	1

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