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  3457  suppssfv  6057  suppssov1  6058  nnmord  6496  findcard2  6867  findcard2s  6868  addn0nid  8293  nn0n0n1ge2  9282  xnegdi  9825  efne0  11641  divgcdcoprmex  12056  pceulem  12248  pcqmul  12257  pcqcl  12260  pcaddlem  12292  pcadd  12293  grpinvnz  12770
  Copyright terms: Public domain W3C validator