Theorem necon3d 2464

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1402   =/= wne 2420

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 623  ax-in2 624

This theorem depends on definitions:  df-bi 117  df-ne 2421

This theorem is referenced by:  necon3i  2468  pm13.18  2501  ssn0  3565  suppssov1  6289  suppfnss  6487  suppssfvg  6493  nnmord  6780  findcard2  7183  findcard2s  7184  addn0nid  8690  nn0n0n1ge2  9694  xnegdi  10249  efne0  12423  divgcdcoprmex  12858  pceulem  13051  pcqmul  13060  pcqcl  13063  pcaddlem  13096  pcadd  13097  grpinvnz  13853  ringelnzr  14467  lmodfopne  14635  lmodindp1  14737  clwwlkccat  16556  clwwlknonel  16587