Theorem necon3d 2404

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 2402	. 2 |- ( ph -> ( C =/= D -> -. A = B ) )
3		df-ne 2361	. 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 2360

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 2361

This theorem is referenced by:  necon3i  2408  pm13.18  2441  ssn0  3480  suppssfv  6102  suppssov1  6103  nnmord  6542  findcard2  6917  findcard2s  6918  addn0nid  8361  nn0n0n1ge2  9353  xnegdi  9898  efne0  11718  divgcdcoprmex  12134  pceulem  12326  pcqmul  12335  pcqcl  12338  pcaddlem  12371  pcadd  12372  grpinvnz  13015  ringelnzr  13534  lmodfopne  13642  lmodindp1  13744