Theorem necon3d 2447

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 2445	. 2 |- ( ph -> ( C =/= D -> -. A = B ) )
3		df-ne 2404	. 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 2403

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 2404

This theorem is referenced by:  necon3i  2451  pm13.18  2484  ssn0  3539  suppssov1  6241  suppfnss  6435  suppssfvg  6441  nnmord  6728  findcard2  7121  findcard2s  7122  addn0nid  8595  nn0n0n1ge2  9594  xnegdi  10147  efne0  12302  divgcdcoprmex  12737  pceulem  12930  pcqmul  12939  pcqcl  12942  pcaddlem  12975  pcadd  12976  grpinvnz  13717  ringelnzr  14265  lmodfopne  14405  lmodindp1  14507  clwwlkccat  16325  clwwlknonel  16356