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

Theorem necon4bd 2674
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 2667 . 2  |-  ( ph  ->  ( A  =  B  ->  -.  -.  ps )
)
3 notnot2 112 . 2  |-  ( -. 
-.  ps  ->  ps )
42, 3syl6 33 1  |-  ( ph  ->  ( A  =  B  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1370    =/= wne 2648
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 2650
This theorem is referenced by:  om00  7127  pw2f1olem  7528  xlt2add  11338  hashtpg  12308  hashfun  12321  fsumcl2lem  13330  gcdeq0  13827  phibndlem  13967  abvn0b  17507  cfinufil  19643  isxmet2d  20044  i1fres  21326  tdeglem4  21672  ply1domn  21738  pilem2  22060  isnsqf  22616  ppieq0  22657  chpeq0  22690  chteq0  22691  fprodcl2lem  27630  ltrnatlw  34190
  Copyright terms: Public domain W3C validator