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

Theorem eqneqall 2793
 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 2782 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 pm2.24 120 . 2 (𝐴 = 𝐵 → (¬ 𝐴 = 𝐵𝜑))
31, 2syl5bi 231 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:  nonconne  2794  ssprsseq  4297  prnebg  4329  propssopi  4896  iunopeqop  4906  tpres  6371  elovmpt3imp  6788  bropopvvv  7142  bropfvvvvlem  7143  fin1a2lem10  9114  modfzo0difsn  12604  suppssfz  12656  hashrabsn1  13024  hash2pwpr  13115  hashge2el2difr  13118  cshwidxmod  13400  cshwidx0  13403  mod2eq1n2dvds  14909  nno  14936  prm2orodd  15242  prm23lt5  15357  dvdsprmpweqnn  15427  symgextf1  17664  01eq0ring  19093  mamufacex  20014  mavmulsolcl  20176  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  lgsqrmodndvds  24878  gausslemma2dlem0f  24886  gausslemma2dlem0i  24889  2lgs  24932  2lgsoddprm  24941  upgredg  25811  umgrnloop2  25817  usgra2edg  25911  wlk0  26289  clwwlkgt0  26299  clwwlknprop  26300  nbhashuvtx1  26442  rusgrasn  26472  frgrawopreglem4  26574  frgraregord13  26646  frgraogt3nreg  26647  goldbachth  39997  lighneallem2  40061  lighneal  40066  uhgr2edg  40435  uvtxa01vtx0  40623  g01wlk0  40860  1wlkreslem  40878  upgrwlkdvdelem  40942  uspgrn2crct  41011  wspn0  41131  2pthdlem1  41137  2pthon3v-av  41150  umgr2adedgspth  41155  umgrclwwlksge2  41219  lppthon  41318  1pthon2v-av  41320  frgrwopreglem4  41484  av-frgrareg  41548  av-frgraregord13  41550  av-frgraogt3nreg  41551  lidldomn1  41711  nzerooringczr  41864  ztprmneprm  41918  suppmptcfin  41954  linc1  42008  lindsrng01  42051  ldepspr  42056  zlmodzxznm  42080
 Copyright terms: Public domain W3C validator