Theorem necon2d 2817

Description: Contrapositive inference for inequality. (Contributed by NM, 28-Dec-2008.)

Hypothesis

Ref	Expression
necon2d.1	|- ( ph -> ( A = B -> C =/= D ) )

Assertion

Ref	Expression
necon2d	|- ( ph -> ( C = D -> A =/= B ) )

Proof of Theorem necon2d

Step	Hyp	Ref	Expression
1		necon2d.1	. . 3 |- ( ph -> ( A = B -> C =/= D ) )
2		df-ne 2795	. . 3 |- ( C =/= D <-> -. C = D )
3	1, 2	syl6ib 241	. 2 |- ( ph -> ( A = B -> -. C = D ) )
4	3	necon2ad 2809	1 |- ( ph -> ( C = D -> A =/= B ) )

Syntax hints:   -. wn 3   -> wi 4   = wceq 1483   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-ne 2795

This theorem is referenced by:  map0g  7897  cantnf  8590  hashprg  13182  hashprgOLD  13183  bcthlem5  23125  deg1ldgn  23853  cxpeq0  24424  lfgrn1cycl  26697  uspgrn2crct  26700  poimirlem17  33426  poimirlem20  33429  poimirlem22  33431  poimirlem27  33436  islshpat  34304  cdleme18b  35579  cdlemh  36105