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  3214  nssne2  3215  disjne  3477  difsn  3730  nbrne1  4023  nbrne2  4024  ac6sfi  6898  indpi  7341  zneo  9354  pc2dvds  12329  pcadd  12339  oddprmdvds  12352  lgsne0  14442
  Copyright terms: Public domain W3C validator