ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  necon3bd Unicode version

Theorem necon3bd 2390
Description: Contrapositive law deduction for inequality. (Contributed by NM, 2-Apr-2007.) (Proof rewritten by Jim Kingdon, 15-May-2018.)
Hypothesis
Ref Expression
necon3bd.1  |-  ( ph  ->  ( A  =  B  ->  ps ) )
Assertion
Ref Expression
necon3bd  |-  ( ph  ->  ( -.  ps  ->  A  =/=  B ) )

Proof of Theorem necon3bd
StepHypRef Expression
1 necon3bd.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  ps ) )
21con3d 631 . 2  |-  ( ph  ->  ( -.  ps  ->  -.  A  =  B ) )
3 df-ne 2348 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3imbitrrdi 162 1  |-  ( ph  ->  ( -.  ps  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1353    =/= wne 2347
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615
This theorem depends on definitions:  df-bi 117  df-ne 2348
This theorem is referenced by:  nelne1  2437  nelne2  2438  nssne1  3215  nssne2  3216  disjne  3478  difsn  3731  nbrne1  4024  nbrne2  4025  ac6sfi  6900  indpi  7343  zneo  9356  pc2dvds  12331  pcadd  12341  oddprmdvds  12354  lssvneln0  13464  lgsne0  14478
  Copyright terms: Public domain W3C validator