Theorem necon3d 2444

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

Syntax hints:   -. wn 3   -> wi 4   = wceq 1395   =/= wne 2400

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 617  ax-in2 618

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

This theorem is referenced by:  necon3i  2448  pm13.18  2481  ssn0  3534  suppssfv  6214  suppssov1  6215  nnmord  6663  findcard2  7051  findcard2s  7052  addn0nid  8520  nn0n0n1ge2  9517  xnegdi  10064  efne0  12189  divgcdcoprmex  12624  pceulem  12817  pcqmul  12826  pcqcl  12829  pcaddlem  12862  pcadd  12863  grpinvnz  13604  ringelnzr  14151  lmodfopne  14290  lmodindp1  14392