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

Theorem necon2bd 2639
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 2623 . . 3  |-  ( A  =/=  B  <->  -.  A  =  B )
31, 2syl6ib 230 . 2  |-  ( ph  ->  ( ps  ->  -.  A  =  B )
)
43con2d 119 1  |-  ( ph  ->  ( A  =  B  ->  -.  ps )
)
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1443    =/= wne 2621
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 189  df-ne 2623
This theorem is referenced by:  necon4bd  2643  necon4d  2647  disjiun  4392  eceqoveq  7465  en3lp  8118  infpssrlem5  8734  nneo  11016  zeo2  11019  sqrt2irr  14294  coprm  14650  dfphi2  14715  pltirr  16202  oddvdsnn0  17186  psgnodpmr  19151  supnfcls  21028  flimfnfcls  21036  metds0  21860  metdseq0  21864  metnrmlem1a  21868  metds0OLD  21875  metdseq0OLD  21879  metnrmlem1aOLD  21883  sineq0  23469  lgsqr  24267  staddi  27892  stadd3i  27894  eulerpartlems  29186  erdszelem8  29914  finminlem  30967  ordcmp  31100  poimirlem18  31951  poimirlem21  31954  cvrnrefN  32842  trlnidatb  33737  bezoutr1  35830
  Copyright terms: Public domain W3C validator