Theorem necon3d 2446

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 2444	. 2 |- ( ph -> ( C =/= D -> -. A = B ) )
3		df-ne 2403	. 2 |- ( A =/= B <-> -. A = B )
4	2, 3	imbitrrdi 162	1 |- ( ph -> ( C =/= D -> A =/= B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1397   =/= wne 2402

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 619  ax-in2 620

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

This theorem is referenced by:  necon3i  2450  pm13.18  2483  ssn0  3537  suppssfv  6231  suppssov1  6232  nnmord  6685  findcard2  7078  findcard2s  7079  addn0nid  8553  nn0n0n1ge2  9550  xnegdi  10103  efne0  12244  divgcdcoprmex  12679  pceulem  12872  pcqmul  12881  pcqcl  12884  pcaddlem  12917  pcadd  12918  grpinvnz  13659  ringelnzr  14207  lmodfopne  14346  lmodindp1  14448  clwwlkccat  16258  clwwlknonel  16289