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

Theorem necon2ad 2507
Description: Contrapositive inference for inequality. (Contributed by NM, 19-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon2ad.1  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)
Assertion
Ref Expression
necon2ad  |-  ( ph  ->  ( ps  ->  A  =/=  B ) )

Proof of Theorem necon2ad
StepHypRef Expression
1 nne 2463 . . 3  |-  ( -.  A  =/=  B  <->  A  =  B )
2 necon2ad.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)
31, 2syl5bi 208 . 2  |-  ( ph  ->  ( -.  A  =/= 
B  ->  -.  ps )
)
43con4d 97 1  |-  ( ph  ->  ( ps  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  necon2d  2509  tz7.2  4393  nordeq  4427  omxpenlem  6979  pr2ne  7651  cflim2  7905  cfslb2n  7910  ltne  8933  sqr2irr  12543  rpexp  12815  pcgcd1  12945  plttr  14120  odhash3  14903  lbspss  15851  nzrunit  16034  en2top  16739  fbfinnfr  17552  ufileu  17630  alexsubALTlem4  17760  lebnumlem1  18475  lebnumlem2  18476  lebnumlem3  18477  ivthlem2  18828  ivthlem3  18829  dvne0  19374  deg1nn0clb  19492  lgsmod  20576  normgt0  21722  nofulllem4  24430  axlowdimlem16  24657  xrltneNEW  27760  prneimg  28183  islln2a  30328  islpln2a  30359  islvol2aN  30403  dalem1  30470  trlnidatb  30988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-ne 2461
  Copyright terms: Public domain W3C validator