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  6212  suppssov1  6213  nnmord  6661  findcard2  7047  findcard2s  7048  addn0nid  8516  nn0n0n1ge2  9513  xnegdi  10060  efne0  12184  divgcdcoprmex  12619  pceulem  12812  pcqmul  12821  pcqcl  12824  pcaddlem  12857  pcadd  12858  grpinvnz  13599  ringelnzr  14145  lmodfopne  14284  lmodindp1  14386