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  3467  suppssfv  6081  suppssov1  6082  nnmord  6520  findcard2  6891  findcard2s  6892  addn0nid  8333  nn0n0n1ge2  9325  xnegdi  9870  efne0  11688  divgcdcoprmex  12104  pceulem  12296  pcqmul  12305  pcqcl  12308  pcaddlem  12340  pcadd  12341  grpinvnz  12946  ringelnzr  13333  lmodfopne  13421
  Copyright terms: Public domain W3C validator