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

Theorem eqneqall 2955
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 2945 . 2 (𝐴𝐵 ↔ ¬ 𝐴 = 𝐵)
2 pm2.24 124 . 2 (𝐴 = 𝐵 → (¬ 𝐴 = 𝐵𝜑))
31, 2biimtrid 241 1 (𝐴 = 𝐵 → (𝐴𝐵𝜑))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4   = wceq 1542  wne 2944
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 206  df-ne 2945
This theorem is referenced by:  nonconne  2956  ssprsseq  4790  prnebg  4818  preqsnd  4821  preq12nebg  4825  prel12g  4826  opthprneg  4827  3elpr2eq  4869  snopeqop  5468  propssopi  5470  opthhausdorff  5479  opthhausdorff0  5480  iunopeqop  5483  tpres  7155  elovmpt3imp  7615  bropopvvv  8027  bropfvvvvlem  8028  infsupprpr  9447  epnsym  9552  eldju2ndl  9867  eldju2ndr  9868  fin1a2lem10  10352  modfzo0difsn  13855  suppssfz  13906  hashrabsn1  14281  hash2pwpr  14382  hashle2pr  14383  hashge2el2difr  14387  cshwidxmod  14698  cshwidx0  14701  mod2eq1n2dvds  16236  nno  16271  prm2orodd  16574  prm23lt5  16693  dvdsprmpweqnn  16764  symgextf1  19210  01eq0ring  20758  mamufacex  21754  mavmulsolcl  21916  chfacfscmulgsum  22225  chfacfpmmulgsum  22229  logbgcd1irr  26160  lgsqrmodndvds  26717  gausslemma2dlem0f  26725  gausslemma2dlem0i  26728  2lgs  26771  2lgsoddprm  26780  2sqreultlem  26811  2sqreunnltlem  26814  umgrnloop2  28139  uhgr2edg  28198  uvtx01vtx  28387  g0wlk0  28642  wlkreslem  28659  upgrwlkdvdelem  28726  uspgrn2crct  28795  wspn0  28911  2pthdlem1  28917  2pthon3v  28930  umgr2adedgspth  28935  umgrclwwlkge2  28977  lppthon  29137  1pthon2v  29139  frgrwopreglem4a  29296  frgrreg  29380  frgrregord13  29382  frgrogt3nreg  29383  nsnlplig  29465  nsnlpligALT  29466  gonarlem  34028  gonar  34029  goalrlem  34030  goalr  34031  bj-prmoore  35615  prproropf1olem4  45772  paireqne  45777  goldbachth  45813  lighneallem2  45872  lighneal  45877  requad1  45888  evenltle  45983  fppr2odd  45997  lidldomn1  46293  nzerooringczr  46444  ztprmneprm  46497  suppmptcfin  46529  linc1  46580  lindsrng01  46623  ldepspr  46628  zlmodzxznm  46652  rrx2xpref1o  46878  rrx2plord2  46882  line2ylem  46911  line2xlem  46913  line2y  46915  inlinecirc02plem  46946
  Copyright terms: Public domain W3C validator