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

Theorem necon4ad 2670
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 115 . 2  |-  ( ph  ->  ( ps  ->  -.  A  =/=  B ) )
3 nne 2610 . 2  |-  ( -.  A  =/=  B  <->  A  =  B )
42, 3syl6ib 226 1  |-  ( ph  ->  ( ps  ->  A  =  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1369    =/= wne 2604
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 185  df-ne 2606
This theorem is referenced by:  necon1d  2678  fisseneq  7522  f1finf1o  7537  dfac5  8296  isf32lem9  8528  fpwwe2  8808  qextlt  11171  qextle  11172  xsubge0  11222  hashf1  12208  climuni  13028  rpnnen2  13506  fzo0dvdseq  13584  4sqlem11  14014  haust1  18954  deg1lt0  21560  ply1divmo  21605  ig1peu  21641  dgrlt  21731  quotcan  21773  fta  22415  atcv0eq  25781  erdszelem9  27085  jm2.19  29339  jm2.26lem3  29347  dgraa0p  29503  lshpdisj  32629  lsatcv0eq  32689  exatleN  33045  atcvr0eq  33067  cdlemg31c  34340
  Copyright terms: Public domain W3C validator