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

Theorem necon4ad 2667
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 110 . 2  |-  ( ph  ->  ( ps  ->  -.  A  =/=  B ) )
3 nne 2607 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3syl6ib 219 1  |-  ( ph  ->  ( ps  ->  A  =  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1653    =/= wne 2601
This theorem is referenced by:  necon1d  2675  fisseneq  7322  f1finf1o  7337  dfac5  8011  isf32lem9  8243  fpwwe2  8520  qextlt  10791  qextle  10792  xsubge0  10842  hashf1  11708  climuni  12348  rpnnen2  12827  fzo0dvdseq  12904  4sqlem11  13325  haust1  17418  deg1lt0  20016  ply1divmo  20060  ig1peu  20096  dgrlt  20186  quotcan  20228  fta  20864  atcv0eq  23884  erdszelem9  24887  jm2.19  27066  jm2.26lem3  27074  dgraa0p  27333  lshpdisj  29847  lsatcv0eq  29907  exatleN  30263  atcvr0eq  30285  cdlemg31c  31558
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 179  df-ne 2603
  Copyright terms: Public domain W3C validator