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

Theorem eqneqall 2801
 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 2791 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 pm2.24 121 . 2 (𝐴 = 𝐵 → (¬ 𝐴 = 𝐵𝜑))
31, 2syl5bi 232 1 (𝐴 = 𝐵 → (𝐴𝐵𝜑))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   = wceq 1480   ≠ wne 2790 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 197  df-ne 2791 This theorem is referenced by:  nonconne  2802  ssprsseq  4325  prnebg  4357  propssopi  4931  iunopeqop  4941  tpres  6420  elovmpt3imp  6843  bropopvvv  7200  bropfvvvvlem  7201  fin1a2lem10  9175  modfzo0difsn  12682  suppssfz  12734  hashrabsn1  13103  hash2pwpr  13196  hashle2pr  13197  hashge2el2difr  13201  cshwidxmod  13486  cshwidx0  13489  mod2eq1n2dvds  14995  nno  15022  prm2orodd  15328  prm23lt5  15443  dvdsprmpweqnn  15513  symgextf1  17762  01eq0ring  19191  mamufacex  20114  mavmulsolcl  20276  chfacfscmulgsum  20584  chfacfpmmulgsum  20588  lgsqrmodndvds  24978  gausslemma2dlem0f  24986  gausslemma2dlem0i  24989  2lgs  25032  2lgsoddprm  25041  umgrnloop2  25934  uhgr2edg  25993  uvtxa01vtx0  26184  g0wlk0  26417  wlkreslem  26435  upgrwlkdvdelem  26501  uspgrn2crct  26569  wspn0  26689  2pthdlem1  26695  2pthon3v  26708  umgr2adedgspth  26713  umgrclwwlksge2  26778  lppthon  26877  1pthon2v  26879  frgrwopreglem4  27042  frgrreg  27106  frgrregord13  27108  frgrogt3nreg  27109  goldbachth  40758  lighneallem2  40822  lighneal  40827  lidldomn1  41209  nzerooringczr  41360  ztprmneprm  41413  suppmptcfin  41448  linc1  41502  lindsrng01  41545  ldepspr  41550  zlmodzxznm  41574
 Copyright terms: Public domain W3C validator