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

Theorem eqneqall 2674
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 2664 . 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 1379    =/= wne 2662
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 2664
This theorem is referenced by:  nonconne  2675  elovmpt3imp  6528  suppssfz  12080  hashrabsn1  12422  hash2prd  12499  hash2pwpr  12500  cshwidxmod  12754  cshwidx0  12756  symgextf1  16318  01eq0ring  17790  mamufacex  18760  mavmulsolcl  18922  chfacfscmulgsum  19230  chfacfpmmulgsum  19234  wlk0  24584  clwwlkgt0  24594  clwwlknprop  24595  nbhashuvtx1  24738  rusgrasn  24768  frgraregord13  24943  frgraogt3nreg  24944  lidldomn1  32321  ztprmneprm  32415  suppmptcfin  32454  linc1  32508  lindsrng01  32551  ldepspr  32556  zlmodzxznm  32580
  Copyright terms: Public domain W3C validator