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

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

Proof of Theorem necon4bd
StepHypRef Expression
1 necon4bd.1 . . 3  |-  ( ph  ->  ( -.  ps  ->  A  =/=  B ) )
21necon2bd 2618 . 2  |-  ( ph  ->  ( A  =  B  ->  -.  -.  ps )
)
3 notnot2 112 . 2  |-  ( -. 
-.  ps  ->  ps )
42, 3syl6 31 1  |-  ( ph  ->  ( A  =  B  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1405    =/= wne 2598
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 2600
This theorem is referenced by:  om00  7261  pw2f1olem  7659  xlt2add  11505  hashfun  12544  hashtpg  12572  fsumcl2lem  13702  fprodcl2lem  13909  gcdeq0  14368  phibndlem  14509  abvn0b  18271  cfinufil  20721  isxmet2d  21122  i1fres  22404  tdeglem4  22750  ply1domn  22816  pilem2  23139  isnsqf  23790  ppieq0  23831  chpeq0  23864  chteq0  23865  ltrnatlw  33201  lcmeq0  36054  bcc0  36093
  Copyright terms: Public domain W3C validator