Theorem necon3d 2421

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1373   =/= wne 2377

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 2378

This theorem is referenced by:  necon3i  2425  pm13.18  2458  ssn0  3507  suppssfv  6167  suppssov1  6168  nnmord  6616  findcard2  7001  findcard2s  7002  addn0nid  8466  nn0n0n1ge2  9463  xnegdi  10010  efne0  12064  divgcdcoprmex  12499  pceulem  12692  pcqmul  12701  pcqcl  12704  pcaddlem  12737  pcadd  12738  grpinvnz  13478  ringelnzr  14024  lmodfopne  14163  lmodindp1  14265