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

Theorem necon4bd 2656
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 2652 . 2  |-  ( ph  ->  ( A  =  B  ->  -.  -.  ps )
)
3 notnot2 117 . 2  |-  ( -. 
-.  ps  ->  ps )
42, 3syl6 34 1  |-  ( ph  ->  ( A  =  B  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1455    =/= wne 2633
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 190  df-ne 2635
This theorem is referenced by:  om00  7307  pw2f1olem  7707  xlt2add  11580  hashfun  12648  hashtpg  12680  fsumcl2lem  13852  fprodcl2lem  14059  gcdeq0  14540  lcmeq0  14620  lcmfeq0b  14658  phibndlem  14773  abvn0b  18581  cfinufil  20998  isxmet2d  21397  i1fres  22719  tdeglem4  23065  ply1domn  23128  pilem2  23463  pilem2OLD  23464  isnsqf  24118  ppieq0  24159  chpeq0  24192  chteq0  24193  ltrnatlw  33795  bcc0  36734
  Copyright terms: Public domain W3C validator