Theorem necon3d 2384

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 2382	. 2 |- ( ph -> ( C =/= D -> -. A = B ) )
3		df-ne 2341	. 2 |- ( A =/= B <-> -. A = B )
4	2, 3	syl6ibr 161	1 |- ( ph -> ( C =/= D -> A =/= B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1348   =/= wne 2340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610

This theorem depends on definitions:  df-bi 116  df-ne 2341

This theorem is referenced by:  necon3i  2388  pm13.18  2421  ssn0  3456  suppssfv  6055  suppssov1  6056  nnmord  6494  findcard2  6865  findcard2s  6866  addn0nid  8286  nn0n0n1ge2  9275  xnegdi  9818  efne0  11634  divgcdcoprmex  12049  pceulem  12241  pcqmul  12250  pcqcl  12253  pcaddlem  12285  pcadd  12286