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

Theorem eqneqall 2724
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 2622 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
2 pm2.24 109 . 2  |-  ( A  =  B  ->  ( -.  A  =  B  ->  ph ) )
31, 2syl5bi 217 1  |-  ( A  =  B  ->  ( A  =/=  B  ->  ph )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1369    =/= wne 2620
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 185  df-ne 2622
This theorem is referenced by:  hash2prd  12200  hash2pwpr  12201  cshwidxmod  12459  cshwidx0  12461  symgextf1  15945  mamufacex  18308  mavmulsolcl  18381  elovmpt3imp  30183  hashrabsn1  30256  wlk0  30315  clwwlkgt0  30457  clwwlknprop  30458  nbhashuvtx1  30556  rusgrasn  30580  frgraregord13  30735  frgraogt3nreg  30736  ztprmneprm  30762  01eq0rng  30800  suppssfz  30809  suppmptcfin  30816  linc1  30982  lindsrng01  31025  ldepspr  31030  zlmodzxznm  31062
  Copyright terms: Public domain W3C validator