Theorem necon3d 2444

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

Step	Hyp	Ref	Expression
1		necon3d.1	. . 3 |- ( ph -> ( A = B -> C = D ) )
2	1	necon3ad 2442	. 2 |- ( ph -> ( C =/= D -> -. A = B ) )
3		df-ne 2401	. 2 |- ( A =/= B <-> -. A = B )
4	2, 3	imbitrrdi 162	1 |- ( ph -> ( C =/= D -> A =/= B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1395   =/= wne 2400

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 617  ax-in2 618

This theorem depends on definitions:  df-bi 117  df-ne 2401

This theorem is referenced by:  necon3i  2448  pm13.18  2481  ssn0  3535  suppssfv  6226  suppssov1  6227  nnmord  6680  findcard2  7071  findcard2s  7072  addn0nid  8543  nn0n0n1ge2  9540  xnegdi  10093  efne0  12229  divgcdcoprmex  12664  pceulem  12857  pcqmul  12866  pcqcl  12869  pcaddlem  12902  pcadd  12903  grpinvnz  13644  ringelnzr  14191  lmodfopne  14330  lmodindp1  14432  clwwlkccat  16196  clwwlknonel  16227