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

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

Proof of Theorem necon4ad
StepHypRef Expression
1 notnot1 122 . 2  |-  ( ps 
->  -.  -.  ps )
2 necon4ad.1 . . 3  |-  ( ph  ->  ( A  =/=  B  ->  -.  ps ) )
32necon1bd 2661 . 2  |-  ( ph  ->  ( -.  -.  ps  ->  A  =  B ) )
41, 3syl5 32 1  |-  ( ph  ->  ( ps  ->  A  =  B ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1383    =/= wne 2638
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 2640
This theorem is referenced by:  necon1d  2668  fisseneq  7733  f1finf1o  7748  dfac5  8512  isf32lem9  8744  fpwwe2  9024  qextlt  11413  qextle  11414  xsubge0  11464  hashf1  12488  climuni  13357  rpnnen2  13941  fzo0dvdseq  14021  4sqlem11  14455  haust1  19831  deg1lt0  22469  ply1divmo  22514  ig1peu  22550  dgrlt  22641  quotcan  22683  fta  23331  atcv0eq  27276  erdszelem9  28621  jm2.19  30911  jm2.26lem3  30919  dgraa0p  31074  lshpdisj  34587  lsatcv0eq  34647  exatleN  35003  atcvr0eq  35025  cdlemg31c  36300
  Copyright terms: Public domain W3C validator