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

Theorem eqneqall 2834
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 2824 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 pm2.24 121 . 2 (𝐴 = 𝐵 → (¬ 𝐴 = 𝐵𝜑))
31, 2syl5bi 232 1 (𝐴 = 𝐵 → (𝐴𝐵𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1523  wne 2823
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 2824
This theorem is referenced by:  nonconne  2835  ssprsseq  4389  prnebg  4420  3elpr2eq  4467  propssopi  5000  iunopeqop  5010  tpres  6507  elovmpt3imp  6932  bropopvvv  7300  bropfvvvvlem  7301  fin1a2lem10  9269  modfzo0difsn  12782  suppssfz  12834  hashrabsn1  13201  hash2pwpr  13296  hashle2pr  13297  hashge2el2difr  13301  cshwidxmod  13595  cshwidx0  13598  mod2eq1n2dvds  15118  nno  15145  prm2orodd  15451  prm23lt5  15566  dvdsprmpweqnn  15636  symgextf1  17887  01eq0ring  19320  mamufacex  20243  mavmulsolcl  20405  chfacfscmulgsum  20713  chfacfpmmulgsum  20717  lgsqrmodndvds  25123  gausslemma2dlem0f  25131  gausslemma2dlem0i  25134  2lgs  25177  2lgsoddprm  25186  umgrnloop2  26086  uhgr2edg  26145  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  g0wlk0  26604  wlkreslem  26622  upgrwlkdvdelem  26688  uspgrn2crct  26756  wspn0  26889  2pthdlem1  26895  2pthon3v  26908  umgr2adedgspth  26913  umgrclwwlkge2  26957  lppthon  27129  1pthon2v  27131  frgrwopreglem4a  27290  frgrreg  27381  frgrregord13  27383  frgrogt3nreg  27384  nsnlplig  27463  nsnlpligALT  27464  goldbachth  41784  lighneallem2  41848  lighneal  41853  evenltle  41951  lidldomn1  42246  nzerooringczr  42397  ztprmneprm  42450  suppmptcfin  42485  linc1  42539  lindsrng01  42582  ldepspr  42587  zlmodzxznm  42611
  Copyright terms: Public domain W3C validator