Theorem necon3d 2458

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 2456	. 2 |- ( ph -> ( C =/= D -> -. A = B ) )
3		df-ne 2415	. 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 2414

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 2415

This theorem is referenced by:  necon3i  2462  pm13.18  2495  ssn0  3555  suppssov1  6272  suppfnss  6470  suppssfvg  6476  nnmord  6763  findcard2  7159  findcard2s  7160  addn0nid  8663  nn0n0n1ge2  9665  xnegdi  10220  efne0  12389  divgcdcoprmex  12824  pceulem  13017  pcqmul  13026  pcqcl  13029  pcaddlem  13062  pcadd  13063  grpinvnz  13826  ringelnzr  14432  lmodfopne  14600  lmodindp1  14702  clwwlkccat  16522  clwwlknonel  16553