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

Theorem necon2bd 2646
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 2627 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2syl6ib 229 . 2  |-  ( ph  ->  ( ps  ->  -.  A  =  B )
)
43con2d 118 1  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1437    =/= wne 2625
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 188  df-ne 2627
This theorem is referenced by:  necon4bd  2653  necon4d  2658  disjiun  4417  eceqoveq  7476  en3lp  8121  infpssrlem5  8735  nneo  11019  zeo2  11022  sqrt2irr  14279  coprm  14628  dfphi2  14691  pltirr  16160  oddvdsnn0  17135  psgnodpmr  19089  supnfcls  20966  flimfnfcls  20974  metds0  21778  metdseq0  21782  metnrmlem1a  21786  sineq0  23341  lgsqr  24137  staddi  27734  stadd3i  27736  eulerpartlems  29019  erdszelem8  29709  finminlem  30759  ordcmp  30892  poimirlem18  31662  poimirlem21  31665  cvrnrefN  32557  trlnidatb  33452  bezoutr1  35542
  Copyright terms: Public domain W3C validator