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

Theorem necon4ad 2520
Description: Contrapositive inference for inequality. (Contributed by NM, 2-Apr-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypothesis
Ref Expression
necon4ad.1  |-  ( ph  ->  ( A  =/=  B  ->  -.  ps ) )
Assertion
Ref Expression
necon4ad  |-  ( ph  ->  ( ps  ->  A  =  B ) )

Proof of Theorem necon4ad
StepHypRef Expression
1 necon4ad.1 . . 3  |-  ( ph  ->  ( A  =/=  B  ->  -.  ps ) )
21con2d 107 . 2  |-  ( ph  ->  ( ps  ->  -.  A  =/=  B ) )
3 nne 2463 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3syl6ib 217 1  |-  ( ph  ->  ( ps  ->  A  =  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1632    =/= wne 2459
This theorem is referenced by:  necon1d  2528  fisseneq  7090  f1finf1o  7102  dfac5  7771  isf32lem9  8003  fpwwe2  8281  qextlt  10546  qextle  10547  xsubge0  10597  hashf1  11411  climuni  12042  rpnnen2  12520  fzo0dvdseq  12597  4sqlem11  13018  haust1  17096  deg1lt0  19493  ply1divmo  19537  ig1peu  19573  dgrlt  19663  quotcan  19705  fta  20333  atcv0eq  22975  erdszelem9  23745  jm2.19  27189  jm2.26lem3  27197  dgraa0p  27457  lshpdisj  29799  lsatcv0eq  29859  exatleN  30215  atcvr0eq  30237  cdlemg31c  31510
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 177  df-ne 2461
  Copyright terms: Public domain W3C validator