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  6230  suppssov1  6231  nnmord  6684  findcard2  7077  findcard2s  7078  addn0nid  8552  nn0n0n1ge2  9549  xnegdi  10102  efne0  12238  divgcdcoprmex  12673  pceulem  12866  pcqmul  12875  pcqcl  12878  pcaddlem  12911  pcadd  12912  grpinvnz  13653  ringelnzr  14200  lmodfopne  14339  lmodindp1  14441  clwwlkccat  16251  clwwlknonel  16282