Theorem necon3d 2419

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1372   =/= wne 2375

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 615  ax-in2 616

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

This theorem is referenced by:  necon3i  2423  pm13.18  2456  ssn0  3502  suppssfv  6153  suppssov1  6154  nnmord  6602  findcard2  6985  findcard2s  6986  addn0nid  8445  nn0n0n1ge2  9442  xnegdi  9989  efne0  11960  divgcdcoprmex  12395  pceulem  12588  pcqmul  12597  pcqcl  12600  pcaddlem  12633  pcadd  12634  grpinvnz  13374  ringelnzr  13920  lmodfopne  14059  lmodindp1  14161