Theorem necon3d 2411

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1364   =/= wne 2367

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 2368

This theorem is referenced by:  necon3i  2415  pm13.18  2448  ssn0  3494  suppssfv  6135  suppssov1  6136  nnmord  6584  findcard2  6959  findcard2s  6960  addn0nid  8417  nn0n0n1ge2  9413  xnegdi  9960  efne0  11860  divgcdcoprmex  12295  pceulem  12488  pcqmul  12497  pcqcl  12500  pcaddlem  12533  pcadd  12534  grpinvnz  13273  ringelnzr  13819  lmodfopne  13958  lmodindp1  14060