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

Theorem necon2bd 2653
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 2601 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2syl6ib 218 . 2  |-  ( ph  ->  ( ps  ->  -.  A  =  B )
)
43con2d 109 1  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1652    =/= wne 2599
This theorem is referenced by:  necon4d  2667  disjiun  4202  eceqoveq  7009  en3lp  7672  infpssrlem5  8187  nneo  10353  zeo2  10356  sqr2irr  12848  coprm  13100  dfphi2  13163  pltirr  14420  oddvdsnn0  15182  supnfcls  18052  flimfnfcls  18060  metds0  18880  metdseq0  18884  metnrmlem1a  18888  sineq0  20429  lgsqr  21130  staddi  23749  stadd3i  23751  erdszelem8  24884  ordcmp  26197  finminlem  26321  bezoutr1  27051  cvrnrefN  30080  trlnidatb  30974
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 178  df-ne 2601
  Copyright terms: Public domain W3C validator