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

Theorem necon2bd 2616
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 2569 . . 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 1649    =/= wne 2567
This theorem is referenced by:  necon4d  2630  disjiun  4162  eceqoveq  6968  en3lp  7628  infpssrlem5  8143  nneo  10309  zeo2  10312  sqr2irr  12803  coprm  13055  dfphi2  13118  pltirr  14375  oddvdsnn0  15137  supnfcls  18005  flimfnfcls  18013  metds0  18833  metdseq0  18837  metnrmlem1a  18841  sineq0  20382  lgsqr  21083  staddi  23702  stadd3i  23704  erdszelem8  24837  ordcmp  26101  finminlem  26211  bezoutr1  26941  cvrnrefN  29765  trlnidatb  30659
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 2569
  Copyright terms: Public domain W3C validator