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  3534  suppssfv  6220  suppssov1  6221  nnmord  6671  findcard2  7059  findcard2s  7060  addn0nid  8531  nn0n0n1ge2  9528  xnegdi  10076  efne0  12204  divgcdcoprmex  12639  pceulem  12832  pcqmul  12841  pcqcl  12844  pcaddlem  12877  pcadd  12878  grpinvnz  13619  ringelnzr  14166  lmodfopne  14305  lmodindp1  14407  clwwlkccat  16138