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

Theorem necon3d 2391
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 2389 . 2  |-  ( ph  ->  ( C  =/=  D  ->  -.  A  =  B ) )
3 df-ne 2348 . 2  |-  ( A  =/=  B  <->  -.  A  =  B )
42, 3imbitrrdi 162 1  |-  ( ph  ->  ( C  =/=  D  ->  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:  necon3i  2395  pm13.18  2428  ssn0  3465  suppssfv  6078  suppssov1  6079  nnmord  6517  findcard2  6888  findcard2s  6889  addn0nid  8330  nn0n0n1ge2  9322  xnegdi  9867  efne0  11685  divgcdcoprmex  12101  pceulem  12293  pcqmul  12302  pcqcl  12305  pcaddlem  12337  pcadd  12338  grpinvnz  12940  ringelnzr  13326
  Copyright terms: Public domain W3C validator