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

Theorem eqneqall 2589
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 2579 . 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 1399    =/= wne 2577
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 2579
This theorem is referenced by:  nonconne  2590  prnebg  4126  tpres  6026  elovmpt3imp  6432  bropopvvv  6779  fin1a2lem10  8702  suppssfz  12003  hashrabsn1  12345  hash2prd  12422  hash2pwpr  12423  cshwidxmod  12685  cshwidx0  12687  symgextf1  16563  01eq0ring  18033  mamufacex  18976  mavmulsolcl  19138  chfacfscmulgsum  19446  chfacfpmmulgsum  19450  usgra2edg  24503  wlk0  24882  clwwlkgt0  24892  clwwlknprop  24893  nbhashuvtx1  25036  rusgrasn  25066  frgrawopreglem4  25168  frgraregord13  25240  frgraogt3nreg  25241  mod2eq1n2dvds  32462  lidldomn1  32927  nzerooringczr  33080  ztprmneprm  33136  suppmptcfin  33172  linc1  33226  lindsrng01  33269  ldepspr  33274  zlmodzxznm  33298  nno  33338
  Copyright terms: Public domain W3C validator