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

Theorem necon4ad 2687
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 2685 . 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 1379    =/= wne 2662
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 2664
This theorem is referenced by:  necon1d  2692  fisseneq  7731  f1finf1o  7746  dfac5  8509  isf32lem9  8741  fpwwe2  9021  qextlt  11402  qextle  11403  xsubge0  11453  hashf1  12472  climuni  13338  rpnnen2  13820  fzo0dvdseq  13898  4sqlem11  14332  haust1  19647  deg1lt0  22254  ply1divmo  22299  ig1peu  22335  dgrlt  22425  quotcan  22467  fta  23109  atcv0eq  27002  erdszelem9  28311  jm2.19  30567  jm2.26lem3  30575  dgraa0p  30731  lshpdisj  33802  lsatcv0eq  33862  exatleN  34218  atcvr0eq  34240  cdlemg31c  35513
  Copyright terms: Public domain W3C validator