Theorem necon3d 2456

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1398   =/= wne 2412

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 2413

This theorem is referenced by:  necon3i  2460  pm13.18  2493  ssn0  3551  suppssov1  6263  suppfnss  6457  suppssfvg  6463  nnmord  6750  findcard2  7146  findcard2s  7147  addn0nid  8647  nn0n0n1ge2  9648  xnegdi  10201  efne0  12364  divgcdcoprmex  12799  pceulem  12992  pcqmul  13001  pcqcl  13004  pcaddlem  13037  pcadd  13038  grpinvnz  13784  ringelnzr  14332  lmodfopne  14474  lmodindp1  14576  clwwlkccat  16396  clwwlknonel  16427