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

Theorem necon3d 2384
Description: Contrapositive law deduction for inequality. (Contributed by NM, 10-Jun-2006.)
Hypothesis
Ref Expression
necon3d.1  |-  ( ph  ->  ( A  =  B  ->  C  =  D ) )
Assertion
Ref Expression
necon3d  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )

Proof of Theorem necon3d
StepHypRef Expression
1 necon3d.1 . . 3  |-  ( ph  ->  ( A  =  B  ->  C  =  D ) )
21necon3ad 2382 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2341 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3syl6ibr 161 1  |-  ( ph  ->  ( C  =/=  D  ->  A  =/=  B ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    = wceq 1348    =/= wne 2340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610
This theorem depends on definitions:  df-bi 116  df-ne 2341
This theorem is referenced by:  necon3i  2388  pm13.18  2421  ssn0  3456  suppssfv  6055  suppssov1  6056  nnmord  6494  findcard2  6865  findcard2s  6866  addn0nid  8286  nn0n0n1ge2  9275  xnegdi  9818  efne0  11634  divgcdcoprmex  12049  pceulem  12241  pcqmul  12250  pcqcl  12253  pcaddlem  12285  pcadd  12286
  Copyright terms: Public domain W3C validator