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

Theorem necon2bd 2682
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 2664 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2syl6ib 226 . 2  |-  ( ph  ->  ( ps  ->  -.  A  =  B )
)
43con2d 115 1  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)
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:  necon4bd  2689  necon4d  2694  disjiun  4443  eceqoveq  7428  en3lp  8045  infpssrlem5  8699  nneo  10956  zeo2  10959  sqrt2irr  13860  coprm  14117  dfphi2  14180  pltirr  15467  oddvdsnn0  16441  psgnodpmr  18495  supnfcls  20389  flimfnfcls  20397  metds0  21222  metdseq0  21226  metnrmlem1a  21230  sineq0  22780  lgsqr  23487  staddi  26979  stadd3i  26981  eulerpartlems  28115  erdszelem8  28458  ordcmp  29830  finminlem  30054  bezoutr1  30843  cvrnrefN  34435  trlnidatb  35329
  Copyright terms: Public domain W3C validator