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

Theorem eqneqall 2654
Description: A contradiction concerning equality implies anything. (Contributed by Alexander van der Vekens, 25-Jan-2018.)
Assertion
Ref Expression
eqneqall  |-  ( A  =  B  ->  ( A  =/=  B  ->  ph )
)

Proof of Theorem eqneqall
StepHypRef Expression
1 df-ne 2643 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 pm2.24 112 . 2  |-  ( A  =  B  ->  ( -.  A  =  B  ->  ph ) )
31, 2syl5bi 225 1  |-  ( A  =  B  ->  ( A  =/=  B  ->  ph )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1452    =/= wne 2641
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 190  df-ne 2643
This theorem is referenced by:  nonconne  2655  prnebg  4149  tpres  6133  elovmpt3imp  6543  bropopvvv  6893  bropfvvvvlem  6894  fin1a2lem10  8857  modfzo0difsn  12195  suppssfz  12244  hashrabsn1  12591  hash2pwpr  12676  hashge2el2difr  12679  cshwidxmod  12959  cshwidx0  12962  symgextf1  17140  01eq0ring  18573  mamufacex  19491  mavmulsolcl  19653  chfacfscmulgsum  19961  chfacfpmmulgsum  19965  usgra2edg  25188  wlk0  25568  clwwlkgt0  25578  clwwlknprop  25579  nbhashuvtx1  25722  rusgrasn  25752  frgrawopreglem4  25854  frgraregord13  25926  frgraogt3nreg  25927  mod2eq1n2dvds  38870  propssopi  39147  ssprsseq  39149  iunopeqop  39151  upgredg  39389  umgrnloop2  39395  uhgr2edg  39453  uvtxa01vtx0  39633  g01wlk0  39851  1wlkreslem  39865  upgrwlkdvdelem  39928  uspgrn2crct  39986  lppthon  40039  1pthon2v-av  40041  2pthdlem1  40052  2pthon3v-av  40065  umgr2adedgspth  40070  lidldomn1  40429  nzerooringczr  40582  ztprmneprm  40636  suppmptcfin  40672  linc1  40726  lindsrng01  40769  ldepspr  40774  zlmodzxznm  40798  nno  40836
  Copyright terms: Public domain W3C validator