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

Theorem necon4ad 2507
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 2450 . 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 1623    =/= wne 2446
This theorem is referenced by:  necon1d  2515  fisseneq  7074  f1finf1o  7086  dfac5  7755  isf32lem9  7987  fpwwe2  8265  qextlt  10530  qextle  10531  xsubge0  10581  hashf1  11395  climuni  12026  rpnnen2  12504  fzo0dvdseq  12581  4sqlem11  13002  haust1  17080  deg1lt0  19477  ply1divmo  19521  ig1peu  19557  dgrlt  19647  quotcan  19689  fta  20317  atcv0eq  22959  erdszelem9  23141  jm2.19  26498  jm2.26lem3  26506  dgraa0p  26766  lshpdisj  28550  lsatcv0eq  28610  exatleN  28966  atcvr0eq  28988  cdlemg31c  30261
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 2448
  Copyright terms: Public domain W3C validator