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

Theorem necon2bd 2495
Description: Contrapositive inference for inequality. (Contributed by NM, 13-Apr-2007.)
Hypothesis
Ref Expression
necon2bd.1  |-  ( ph  ->  ( ps  ->  A  =/=  B ) )
Assertion
Ref Expression
necon2bd  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)

Proof of Theorem necon2bd
StepHypRef Expression
1 necon2bd.1 . . 3  |-  ( ph  ->  ( ps  ->  A  =/=  B ) )
2 df-ne 2448 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2syl6ib 217 . 2  |-  ( ph  ->  ( ps  ->  -.  A  =  B )
)
43con2d 107 1  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1623    =/= wne 2446
This theorem is referenced by:  necon4d  2509  disjiun  4013  eceqoveq  6763  en3lp  7418  infpssrlem5  7933  nneo  10095  zeo2  10098  sqr2irr  12527  coprm  12779  dfphi2  12842  pltirr  14097  oddvdsnn0  14859  supnfcls  17715  flimfnfcls  17723  metds0  18354  metdseq0  18358  metnrmlem1a  18362  sineq0  19889  lgsqr  20585  staddi  22826  stadd3i  22828  erdszelem8  23729  ordcmp  24886  finminlem  26231  bezoutr1  27073  cvrnrefN  29472  trlnidatb  30366
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 2448
  Copyright terms: Public domain W3C validator